Formal proofs

A proof says something an evaluation cannot: that a property holds in every case of a model, not only in the cases a suite holds. Oloproof keeps a solver's result as evidence, and a release can require one. What a proof is about is the formalized model you wrote down, never the deployment: a proof that every transfer is authorized holds of the permission model, and whether the running system implements that model is a separate question your suites answer.

Keeping a result

A result from any solver comes in under one contract, a JSON file:

{
  "property": {"id": "transfer-authorized", "notation": "LTL", "statement": "G(transfer -> authorized)"},
  "model": {"digest": "sha256:...", "description": "the agent's tool-permission model"},
  "solver": {"name": "nuXmv", "version": "2.0.0"},
  "assumptions": ["the tool router is the only path to transfer"],
  "outcome": "PROVED",
  "scope": "the permission model, not the deployment",
  "produced_at": "2026-10-19T09:00:00Z"
}

oloproof proofs import result.json

The outcome is one of PROVED, DISPROVED, UNKNOWN, TIMEOUT, ERROR or NOT_APPLICABLE, and it is its own field: never a decision state. certificate and counterexample hold what the solver gave, timeout_seconds and environment how it ran. The result is sealed by its content, so an edited copy is a different result. A file that breaks the contract is refused with exit code 2, and so is a produced_at without a time zone or in the future, and a PROVED that carries a counterexample; the schema is schemas/v1/proof_result.schema.json.

Running z3

For SMT-LIB, Oloproof runs one solver itself, z3, when it is on your PATH (brew install z3, apt install z3 or pip install z3-solver). The file asserts the property's negation:

oloproof proofs run transfer.smt2 --property transfer-authorized --statement "every transfer is authorized"

unsat means no counterexample exists in the model: PROVED. sat means one does: DISPROVED, with z3's model as the counterexample when the file asks for it with (get-model). unknown is UNKNOWN, a run past --timeout is TIMEOUT, and anything else is ERROR: several answers, an error after the answer, or a non-zero exit. The one error accepted is z3 saying no model is available after unsat, since there is none to give. oloproof proofs list shows every result the project holds.

A vacuous file reads PROVED: when the model's own assertions contradict each other ((assert false), or two constraints that cannot both hold), unsat cannot tell that from a property that holds. Check that the model is satisfiable without the negated property before you trust a proof of it.

Requiring a proof

proofs:
  - id: no-unauthorized-transfer
    property: transfer-authorized

A proofs: entry in release.yaml is decided at every gate on the last result received for its property, or for the model named by model: (a digest) when you set one. The date a result carries orders nothing, so a result dated later cannot hide one received after it. When a DISPROVED is held for the property, the rule reads it whatever arrived after, so a later PROVED never hides a counterexample, even one of another model: a model's digest is whoever pushed the result's word. To move on to a corrected model, name its digest in model:, and the rule reads that model's results alone. PROVED is PASS and DISPROVED is FAIL. Any other outcome is INSUFFICIENT_EVIDENCE with the reason proof_undecided, and no result at all is INSUFFICIENT_EVIDENCE with proof_missing, so a release that requires a proof waits for one. requires_manual_review: true sends it to review whatever the outcome.

Where it shows

oloproof push carries the results a gate read. Your workspace holds them but cannot rerun a solver or see your model, so it withholds a proof's PASS as MANUAL_REVIEW for a person to read; a FAIL or INSUFFICIENT_EVIDENCE stands. A decision record carries the results its run's gate read, not results imported after it: record verify re-reads each rule's decision from them, fails a result edited after it was sealed, and reports the result itself as the team's word.

Where to go next

• Hazard register covers what can go wrong, which a proof can rule out in the model.
• Gating covers how a rule blocks a release.