形式証明

証明は、評価にはできないことを述べます。あるプロパティが、スイートに含まれるケースだけでなく、モデルのあらゆるケースで成り立つということです。Oloproof はソルバーの結果を証拠として保持し、リリースはそれを要求できます。証明の対象は、あなたが書き下した形式化されたモデルであり、デプロイメントではありません。すべての送金が承認されているという証明は権限モデルについて成り立つもので、稼働中のシステムがそのモデルを実装しているかどうかは別の問いであり、それにはスイートが答えます。

結果を保持する

どのソルバーの結果も、1 つの契約、つまり 1 つの JSON ファイルとして取り込まれます。

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

結論（outcome）は PROVED、DISPROVED、UNKNOWN、TIMEOUT、ERROR、NOT_APPLICABLE のいずれかで、独立したフィールドです。決して決定状態ではありません。certificate と counterexample にはソルバーが出したものを、timeout_seconds と environment にはその実行のしかたを保持します。結果は内容によって封印されるため、編集したコピーは別の結果になります。契約に反するファイルは終了コード 2 で拒否され、タイムゾーンのない、または未来の produced_at、反例を持つ PROVED も同様に拒否されます。スキーマは schemas/v1/proof_result.schema.json です。

z3 を実行する

SMT-LIB については、Oloproof は 1 つのソルバー、z3 を自ら実行します。z3 が PATH 上にある場合です（brew install z3、apt install z3、pip install z3-solver）。ファイルはプロパティの否定を表明します。

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

unsat は、モデルに反例が存在しないことを意味し、PROVED になります。sat は反例が存在することを意味し、DISPROVED になります。ファイルが (get-model) で求めた場合は、z3 のモデルが反例になります。unknown は UNKNOWN、--timeout を超えた実行は TIMEOUT、それ以外はすべて ERROR です。複数の回答、回答の後のエラー、ゼロ以外の終了コードがこれに当たります。受け入れられる唯一のエラーは、unsat の後に z3 がモデルを利用できないと告げるものです。渡すべきモデルが存在しないからです。oloproof proofs list は、プロジェクトが保持するすべての結果を表示します。

空虚なファイルは PROVED になります。モデル自身のアサーションが互いに矛盾する場合（(assert false)、または同時には成り立たない二つの制約）、unsat はそれを成り立つプロパティと区別できません。証明を信頼する前に、否定したプロパティなしでモデルが充足可能であることを確認してください。

証明を要求する

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

release.yaml の proofs: エントリは、各ゲートで、そのプロパティについて最後に受け取った結果に基づいて判定されます。model:（ダイジェスト）を設定した場合は、そのモデルについての結果に基づきます。結果が持つ日付は何の順序も決めないため、後の日付を持つ結果が、その後に受け取った結果を隠すことはできません。そのプロパティについて DISPROVED が保持されている場合、その後に何が届いてもルールはそれを読みます。そのため、後からの PROVED が反例を隠すことは、別のモデルの反例であっても決してありません。モデルのダイジェストは、結果をプッシュした者の申告にすぎないからです。修正したモデルに移るには、そのダイジェストを model: に指定してください。ルールはそのモデルの結果だけを読みます。PROVED は PASS、DISPROVED は FAIL です。それ以外の結論は理由 proof_undecided の INSUFFICIENT_EVIDENCE、結果がまったくない場合は proof_missing の INSUFFICIENT_EVIDENCE となるため、証明を要求するリリースは証明が届くまで待ちます。requires_manual_review: true は、結論にかかわらずレビューに回します。

表示される場所

oloproof push は、ゲートが読んだ結果を運びます。ワークスペースはそれを保持しますが、ソルバーを再実行することもモデルを見ることもできないため、証明の PASS を MANUAL_REVIEW として保留し、人が読むようにします。FAIL や INSUFFICIENT_EVIDENCE はそのまま有効です。決定レコードは、その実行のゲートが読んだ結果を含み、その後にインポートされた結果は含みません。record verify はそこから各ルールの決定を読み直し、封印後に編集された結果を不合格とし、結果そのものはチームの言明として報告します。

次に読むページ

• ハザード登録簿 では、起こりうる不具合を説明します。証明は、それをモデルの中で排除できます。
• Gating では、ルールがリリースを止める仕組みを説明します。