Formale Beweise

Ein Beweis sagt etwas, das eine Evaluation nicht sagen kann: dass eine Eigenschaft in jedem Fall eines Modells gilt, nicht nur in den Fällen, die eine Suite enthält. Oloproof bewahrt das Ergebnis eines Solvers als Evidenz auf, und ein Release kann eines verlangen. Ein Beweis handelt von dem formalisierten Modell, das Sie aufgeschrieben haben, nie vom Deployment: Ein Beweis, dass jede Überweisung autorisiert ist, gilt für das Berechtigungsmodell, und ob das laufende System dieses Modell umsetzt, ist eine eigene Frage, die Ihre Suites beantworten.

Ein Ergebnis aufbewahren

Ein Ergebnis aus jedem beliebigen Solver kommt unter einem Vertrag herein, einer JSON-Datei:

{
  "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

Das Ergebnis ist eines von PROVED, DISPROVED, UNKNOWN, TIMEOUT, ERROR oder NOT_APPLICABLE, und es ist ein eigenes Feld: nie ein Entscheidungszustand. certificate und counterexample enthalten, was der Solver geliefert hat, timeout_seconds und environment, wie er lief. Das Ergebnis ist durch seinen Inhalt versiegelt, eine bearbeitete Kopie ist also ein anderes Ergebnis. Eine Datei, die den Vertrag verletzt, wird mit Exit-Code 2 abgelehnt, ebenso ein produced_at ohne Zeitzone oder in der Zukunft und ein PROVED, das ein Gegenbeispiel trägt; das Schema ist schemas/v1/proof_result.schema.json.

z3 ausführen

Für SMT-LIB führt Oloproof einen Solver selbst aus, z3, wenn er in Ihrem PATH liegt (brew install z3, apt install z3 oder pip install z3-solver). Die Datei behauptet die Negation der Eigenschaft:

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

unsat bedeutet, dass im Modell kein Gegenbeispiel existiert: PROVED. sat bedeutet, dass eines existiert: DISPROVED, mit dem Modell von z3 als Gegenbeispiel, wenn die Datei es mit (get-model) anfordert. unknown ist UNKNOWN, ein Lauf über --timeout hinaus ist TIMEOUT, und alles andere ist ERROR: mehrere Antworten, ein Fehler nach der Antwort oder ein Exit-Code ungleich null. Der einzige akzeptierte Fehler ist die Meldung von z3, nach unsat sei kein Modell verfügbar, denn es gibt keines. oloproof proofs list zeigt jedes Ergebnis, das das Projekt hält.

Eine gegenstandslose Datei liest sich als PROVED: Wenn die eigenen Annahmen des Modells einander widersprechen ((assert false) oder zwei Bedingungen, die nicht beide gelten können), kann unsat das nicht von einer Eigenschaft unterscheiden, die gilt. Prüfen Sie, dass das Modell ohne die negierte Eigenschaft erfüllbar ist, bevor Sie einem Beweis dafür vertrauen.

Einen Beweis verlangen

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

Ein proofs:-Eintrag in release.yaml wird an jedem Gate anhand des zuletzt empfangenen Ergebnisses für seine Eigenschaft entschieden, oder für das mit model: (ein Digest) benannte Modell, wenn Sie eines setzen. Das Datum, das ein Ergebnis trägt, ordnet nichts, ein später datiertes Ergebnis kann also keines verdecken, das nach ihm empfangen wurde. Liegt ein DISPROVED für die Eigenschaft vor, liest die Regel es, gleich was danach kam, sodass ein späteres PROVED nie ein Gegenbeispiel verdeckt, auch nicht eines anderen Modells: Der Digest eines Modells ist das Wort dessen, der das Ergebnis gepusht hat. Um zu einem korrigierten Modell überzugehen, nennen Sie seinen Digest in model:, und die Regel liest allein die Ergebnisse dieses Modells. PROVED ist PASS und DISPROVED ist FAIL. Jedes andere Ergebnis ist INSUFFICIENT_EVIDENCE mit dem Grund proof_undecided, und gar kein Ergebnis ist INSUFFICIENT_EVIDENCE mit proof_missing, sodass ein Release, das einen Beweis verlangt, auf einen wartet. requires_manual_review: true schickt ihn unabhängig vom Ergebnis in die Prüfung.

Wo es erscheint

oloproof push bringt die Ergebnisse mit, die ein Gate gelesen hat. Ihr Workspace hält sie, kann aber keinen Solver erneut ausführen und Ihr Modell nicht sehen, also hält er das PASS eines Beweises als MANUAL_REVIEW zurück, damit ein Mensch es liest; ein FAIL oder INSUFFICIENT_EVIDENCE bleibt bestehen. Ein Entscheidungsdatensatz trägt die Ergebnisse, die das Gate seines Laufs gelesen hat, nicht danach importierte Ergebnisse: record verify liest die Entscheidung jeder Regel daraus neu, lässt ein Ergebnis scheitern, das nach dem Versiegeln bearbeitet wurde, und führt das Ergebnis selbst als Wort des Teams.

Wie es weitergeht

• Gefährdungsregister behandelt, was schiefgehen kann und was ein Beweis im Modell ausschließen kann.
• Gating behandelt, wie eine Regel ein Release blockiert.