Bukti formal

Bukti mengatakan sesuatu yang tidak bisa dikatakan evaluasi: bahwa sebuah properti berlaku di setiap kasus sebuah model, bukan hanya di kasus yang dimuat sebuah suite. Oloproof menyimpan hasil sebuah solver sebagai bukti, dan sebuah rilis dapat mewajibkannya. Yang dibahas sebuah bukti adalah model terformalisasi yang Anda tulis, tidak pernah deployment-nya: bukti bahwa setiap transfer diotorisasi berlaku untuk model izin, dan apakah sistem yang berjalan mengimplementasikan model itu adalah pertanyaan terpisah yang dijawab suite Anda.

Menyimpan hasil

Hasil dari solver mana pun masuk di bawah satu kontrak, sebuah file 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

Hasilnya salah satu dari PROVED, DISPROVED, UNKNOWN, TIMEOUT, ERROR, atau NOT_APPLICABLE, dan itu field tersendiri: tidak pernah sebuah status keputusan. certificate dan counterexample memuat apa yang diberikan solver, timeout_seconds dan environment bagaimana ia dijalankan. Hasil disegel oleh isinya, sehingga salinan yang disunting adalah hasil yang berbeda. File yang melanggar kontrak ditolak dengan kode keluar 2, begitu pula produced_at tanpa zona waktu atau di masa depan, dan PROVED yang membawa contoh penyangkal; skemanya adalah schemas/v1/proof_result.schema.json.

Menjalankan z3

Untuk SMT-LIB, Oloproof menjalankan sendiri satu solver, z3, jika ada di PATH Anda (brew install z3, apt install z3, atau pip install z3-solver). File itu menegaskan negasi properti:

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

unsat berarti tidak ada contoh penyangkal dalam model: PROVED. sat berarti ada satu: DISPROVED, dengan model z3 sebagai contoh penyangkal jika file memintanya dengan (get-model). unknown adalah UNKNOWN, eksekusi yang melewati --timeout adalah TIMEOUT, dan selain itu adalah ERROR: beberapa jawaban, galat setelah jawaban, atau kode keluar bukan nol. Satu-satunya galat yang diterima adalah z3 menyatakan tidak ada model yang tersedia setelah unsat, karena memang tidak ada yang bisa diberikan. oloproof proofs list menampilkan setiap hasil yang dimiliki proyek.

File yang hampa terbaca PROVED: ketika asersi model itu sendiri saling bertentangan ((assert false), atau dua batasan yang tidak dapat berlaku bersamaan), unsat tidak dapat membedakannya dari properti yang berlaku. Periksa bahwa model dapat dipenuhi tanpa negasi properti sebelum Anda memercayai buktinya.

Mewajibkan bukti

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

Entri proofs: di release.yaml diputuskan di setiap gerbang berdasarkan hasil terakhir yang diterima untuk propertinya, atau untuk model yang disebut model: (sebuah digest) jika Anda menetapkannya. Tanggal yang dibawa sebuah hasil tidak mengurutkan apa pun, sehingga hasil bertanggal lebih akhir tidak dapat menyembunyikan hasil yang diterima setelahnya. Ketika DISPROVED dimiliki untuk properti itu, aturan membacanya apa pun yang datang sesudahnya, sehingga PROVED yang lebih akhir tidak pernah menyembunyikan contoh penyangkal, bahkan milik model lain: digest sebuah model adalah kata siapa pun yang mendorong hasil itu. Untuk beralih ke model yang telah diperbaiki, sebutkan digest-nya di model:, dan aturan hanya membaca hasil model itu. PROVED adalah PASS dan DISPROVED adalah FAIL. Hasil lainnya adalah INSUFFICIENT_EVIDENCE dengan alasan proof_undecided, dan tidak ada hasil sama sekali adalah INSUFFICIENT_EVIDENCE dengan proof_missing, sehingga rilis yang mewajibkan bukti menunggunya. requires_manual_review: true mengirimnya ke tinjauan apa pun hasilnya.

Di mana ia tampil

oloproof push membawa hasil yang dibaca sebuah gerbang. Ruang kerja Anda menyimpannya tetapi tidak dapat menjalankan ulang solver atau melihat model Anda, sehingga ia menahan PASS sebuah bukti sebagai MANUAL_REVIEW agar dibaca seseorang; FAIL atau INSUFFICIENT_EVIDENCE tetap berlaku. Rekaman keputusan membawa hasil yang dibaca gerbang run-nya, bukan hasil yang diimpor sesudahnya: record verify membaca ulang keputusan setiap aturan dari hasil itu, menggagalkan hasil yang disunting setelah disegel, dan melaporkan hasil itu sendiri sebagai pernyataan tim.

Langkah selanjutnya

• Daftar bahaya membahas apa yang bisa salah, yang dapat disingkirkan sebuah bukti di dalam model.
• Gating membahas bagaimana sebuah aturan menahan sebuah rilis.