指南
形式化證明
證明能說出評估說不出的事：一個性質在模型的每一種情況下都成立，而不僅僅在套件所含的案例中成立。Oloproof 把求解器的結果作為證據保存，發布可以要求這樣一個結果。證明所針對的是你寫下的形式化模型，從來不是部署本身：證明每筆轉帳都經過授權，這對權限模型成立；而執行中的系統是否實作了該模型，是另一個問題，由你的套件來回答。
保存結果
任何求解器的結果都依同一份契約進入，也就是一個 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結論是 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，當 z3 在你的 PATH 上時（brew install z3、apt install z3 或 pip install z3-solver），Oloproof 會自己執行這一個求解器。檔案斷言的是該性質的否定：
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：多個答案、答案之後出現錯誤，或非零結束。唯一被接受的錯誤是 z3 在 unsat 之後表示沒有可用的模型，因為本來就沒有模型可給。oloproof proofs list 顯示專案保存的每個結果。
一個空真的檔案會讀作 PROVED：當模型自身的斷言相互矛盾時（(assert false)，或兩個不能同時成立的約束），unsat 無法把它與一個成立的性質區分開來。在信任某個性質的證明之前，請先檢查去掉被否定的性質後模型是可滿足的。
要求證明
proofs:
- id: no-unauthorized-transfer
property: transfer-authorizedrelease.yaml 中的 proofs: 條目在每次閘門時，依據為其性質最後收到的結果作出決策；如果你設定了 model:（一個摘要），則依據為該模型最後收到的結果。結果攜帶的日期不決定任何順序，因此日期較晚的結果無法掩蓋在它之後收到的結果。當該性質保存有 DISPROVED 時，無論之後到達的是什麼，規則都會讀取它，因此之後的 PROVED 永遠不會掩蓋反例，即使是另一個模型的反例：模型的摘要只是推送結果者的一面之詞。要換用修正後的模型，請在 model: 中寫明它的摘要，規則便只讀取該模型的結果。PROVED 為 PASS，DISPROVED 為 FAIL。其他任何結論都是 INSUFFICIENT_EVIDENCE，原因為 proof_undecided；完全沒有結果則是 INSUFFICIENT_EVIDENCE，原因為 proof_missing。因此，要求證明的發布會一直等到有證明為止。requires_manual_review: true 無論結論如何都會將其送去審查。
顯示位置
oloproof push 會攜帶閘門讀取過的結果。你的工作區保存這些結果，但無法重新執行求解器，也看不到你的模型，因此它會把證明的 PASS 暫扣為 MANUAL_REVIEW，交由人來閱讀；FAIL 或 INSUFFICIENT_EVIDENCE 則維持不變。決策紀錄會攜帶其執行的閘門讀取過的結果，而不是之後匯入的結果：record verify 依據這些結果重新讀取每條規則的決策，判封存後被編輯的結果失敗，並將結果本身回報為團隊的說法。