指南
形式化证明
证明能说出评估说不出的事：一个性质在模型的每一种情况下都成立，而不仅仅在套件所含的用例中成立。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 依据这些结果重新读取每条规则的决策，判封存后被编辑的结果失败，并将结果本身报告为团队的说法。