Chứng minh hình thức

Một chứng minh nói được điều mà một lần đánh giá không thể nói: rằng một thuộc tính đúng trong mọi trường hợp của một mô hình, không chỉ trong các trường hợp mà một bộ kiểm thử chứa. Oloproof giữ kết quả của một bộ giải (solver) làm bằng chứng, và một bản phát hành có thể yêu cầu một kết quả như vậy. Điều mà một chứng minh nói đến là mô hình đã hình thức hóa mà bạn viết ra, không bao giờ là bản triển khai: một chứng minh rằng mọi giao dịch chuyển tiền đều được ủy quyền thì đúng với mô hình quyền, còn việc hệ thống đang chạy có hiện thực mô hình đó hay không là một câu hỏi riêng mà các bộ kiểm thử của bạn trả lời.

Giữ một kết quả

Kết quả từ bất kỳ bộ giải nào cũng đi vào theo một hợp đồng duy nhất, một tệp 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

Kết cục là một trong PROVED, DISPROVED, UNKNOWN, TIMEOUT, ERROR hoặc NOT_APPLICABLE, và là một trường riêng: không bao giờ là một trạng thái quyết định. certificate và counterexample giữ những gì bộ giải đưa ra, timeout_seconds và environment giữ cách nó đã chạy. Kết quả được niêm phong theo nội dung của nó, nên một bản sao đã chỉnh sửa là một kết quả khác. Một tệp vi phạm hợp đồng bị từ chối với mã thoát 2, cũng như một produced_at không có múi giờ hoặc nằm ở tương lai, và một PROVED mang theo phản ví dụ; schema là schemas/v1/proof_result.schema.json.

Chạy z3

Với SMT-LIB, Oloproof tự chạy một bộ giải, z3, khi nó có trong PATH của bạn (brew install z3, apt install z3 hoặc pip install z3-solver). Tệp khẳng định phủ định của thuộc tính:

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

unsat nghĩa là không tồn tại phản ví dụ nào trong mô hình: PROVED. sat nghĩa là có một phản ví dụ: DISPROVED, với mô hình của z3 làm phản ví dụ khi tệp yêu cầu nó bằng (get-model). unknown là UNKNOWN, một lần chạy vượt quá --timeout là TIMEOUT, và mọi trường hợp khác là ERROR: nhiều câu trả lời, một lỗi sau câu trả lời, hoặc mã thoát khác không. Lỗi duy nhất được chấp nhận là z3 nói không có mô hình nào sau unsat, vì không có mô hình nào để đưa ra. oloproof proofs list hiển thị mọi kết quả mà dự án đang giữ.

Một tệp rỗng nghĩa đọc ra PROVED: khi chính các khẳng định của mô hình mâu thuẫn nhau ((assert false), hoặc hai ràng buộc không thể cùng đúng), unsat không thể phân biệt điều đó với một thuộc tính đúng. Hãy kiểm tra rằng mô hình thỏa mãn được khi không có thuộc tính bị phủ định trước khi tin vào một chứng minh của thuộc tính đó.

Yêu cầu một chứng minh

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

Một mục proofs: trong release.yaml được quyết định ở mỗi cổng dựa trên kết quả cuối cùng nhận được cho thuộc tính của nó, hoặc cho mô hình được nêu bởi model: (một digest) khi bạn đặt một mô hình. Ngày mà một kết quả mang theo không sắp xếp gì cả, nên một kết quả mang ngày muộn hơn không thể che một kết quả nhận được sau nó. Khi một DISPROVED được giữ cho thuộc tính, quy tắc đọc nó bất kể thứ gì đến sau, nên một PROVED sau đó không bao giờ che được một phản ví dụ, kể cả phản ví dụ của mô hình khác: digest của một mô hình là lời của bất kỳ ai đã đẩy kết quả lên. Để chuyển sang một mô hình đã sửa, hãy nêu digest của nó trong model:, và quy tắc chỉ đọc các kết quả của mô hình đó. PROVED là PASS và DISPROVED là FAIL. Mọi kết cục khác là INSUFFICIENT_EVIDENCE với lý do proof_undecided, và không có kết quả nào là INSUFFICIENT_EVIDENCE với proof_missing, nên một bản phát hành yêu cầu chứng minh sẽ chờ có chứng minh. requires_manual_review: true gửi nó đi xem xét bất kể kết cục là gì.

Nơi nó xuất hiện

oloproof push mang theo các kết quả mà một cổng đã đọc. Không gian làm việc của bạn giữ chúng nhưng không thể chạy lại bộ giải hay xem mô hình của bạn, nên nó giữ lại PASS của một chứng minh dưới dạng MANUAL_REVIEW để một người đọc; một FAIL hoặc INSUFFICIENT_EVIDENCE thì được giữ nguyên. Một bản ghi quyết định mang theo các kết quả mà cổng của lần chạy của nó đã đọc, không phải các kết quả được nhập sau đó: record verify đọc lại quyết định của từng quy tắc từ các kết quả đó, đánh trượt một kết quả bị chỉnh sửa sau khi đã niêm phong, và báo chính kết quả là lời của nhóm.

Tiếp theo

• Sổ đăng ký mối nguy nói về những gì có thể xảy ra sai, điều mà một chứng minh có thể loại trừ trong mô hình.
• Gating nói về cách một quy tắc chặn việc phát hành.