가이드
형식 증명
증명은 평가가 말할 수 없는 것을 말합니다. 어떤 속성이 스위트에 담긴 케이스만이 아니라 모델의 모든 케이스에서 성립한다는 것입니다. 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결과값(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의 경우, z3가 PATH에 있으면 Oloproof는 솔버 하나, z3를 직접 실행합니다(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입니다. 여러 개의 답, 답 뒤의 오류, 0이 아닌 종료 코드가 여기에 해당합니다. 허용되는 유일한 오류는 unsat 뒤에 z3가 사용할 수 있는 모델이 없다고 말하는 것으로, 내줄 모델이 없기 때문입니다. 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입니다. 그 밖의 결과값은 사유 proof_undecided의 INSUFFICIENT_EVIDENCE이고, 결과가 아예 없으면 proof_missing의 INSUFFICIENT_EVIDENCE이므로, 증명을 요구하는 릴리스는 증명을 기다립니다. requires_manual_review: true는 결과값과 상관없이 검토로 보냅니다.
표시되는 곳
oloproof push는 게이트가 읽은 결과를 함께 보냅니다. 워크스페이스는 이를 보관하지만 솔버를 다시 실행하거나 모델을 볼 수 없으므로, 증명의 PASS를 MANUAL_REVIEW로 보류해 사람이 읽게 합니다. FAIL이나 INSUFFICIENT_EVIDENCE는 그대로 유지됩니다. 결정 레코드는 그 실행의 게이트가 읽은 결과를 담으며, 그 뒤에 가져온 결과는 담지 않습니다. record verify는 그 결과에서 각 규칙의 결정을 다시 읽고, 봉인된 뒤 편집된 결과를 실패로 처리하며, 결과 자체는 팀의 말로 보고합니다.