Biçimsel ispatlar

Bir ispat, bir değerlendirmenin söyleyemeyeceği bir şeyi söyler: bir özelliğin yalnızca bir süitin içerdiği vakalarda değil, bir modelin her vakasında geçerli olduğunu. Oloproof bir çözücünün (solver) sonucunu kanıt olarak saklar ve bir sürüm böyle bir sonucu şart koşabilir. Bir ispatın konusu, yazdığınız biçimselleştirilmiş modeldir, asla dağıtım değildir: her transferin yetkili olduğuna dair bir ispat izin modeli için geçerlidir; çalışan sistemin bu modeli uygulayıp uygulamadığı ise süitlerinizin yanıtladığı ayrı bir sorudur.

Bir sonucu saklamak

Herhangi bir çözücünün sonucu tek bir sözleşme altında, bir JSON dosyası olarak gelir:

{
  "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

Sonuç PROVED, DISPROVED, UNKNOWN, TIMEOUT, ERROR veya NOT_APPLICABLE değerlerinden biridir ve kendi alanıdır: asla bir karar durumu değildir. certificate ve counterexample çözücünün verdiğini, timeout_seconds ve environment ise nasıl çalıştığını tutar. Sonuç içeriğiyle mühürlenir; bu yüzden düzenlenmiş bir kopya farklı bir sonuçtur. Sözleşmeyi bozan bir dosya 2 çıkış koduyla reddedilir; saat dilimi olmayan ya da gelecekte olan bir produced_at ve karşı örnek taşıyan bir PROVED de öyle; şema schemas/v1/proof_result.schema.json dosyasıdır.

z3'ü çalıştırmak

SMT-LIB için Oloproof bir çözücüyü, z3'ü, PATH üzerinizde bulunduğunda kendisi çalıştırır (brew install z3, apt install z3 veya pip install z3-solver). Dosya, özelliğin olumsuzunu öne sürer:

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

unsat, modelde hiçbir karşı örnek olmadığı anlamına gelir: PROVED. sat bir tane olduğu anlamına gelir: DISPROVED; dosya bunu (get-model) ile istediğinde z3'ün modeli karşı örnek olarak saklanır. unknown, UNKNOWN olur; --timeout süresini aşan bir çalıştırma TIMEOUT, geri kalan her şey ise ERROR olur: birden çok yanıt, yanıttan sonra bir hata ya da sıfır olmayan bir çıkış. Kabul edilen tek hata, z3'ün unsat sonrasında hiçbir model bulunmadığını söylemesidir, çünkü verilecek bir model yoktur. oloproof proofs list, projenin tuttuğu her sonucu gösterir.

Boş yere doğru bir dosya PROVED okunur: modelin kendi önermeleri birbiriyle çeliştiğinde ((assert false) ya da birlikte sağlanamayan iki kısıt), unsat bunu sağlanan bir özellikten ayırt edemez. Bir özelliğin ispatına güvenmeden önce modelin, olumsuzlanmış özellik olmadan sağlanabilir olduğunu kontrol edin.

Bir ispat şart koşmak

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

release.yaml içindeki bir proofs: girdisi, her kapıda özelliği için alınan son sonuca göre, ya da bir tane belirlediğinizde model: (bir özet) ile adlandırılan modele göre karara bağlanır. Bir sonucun taşıdığı tarih hiçbir şeyi sıralamaz; bu yüzden daha geç tarihli bir sonuç, kendisinden sonra alınan bir sonucu gizleyemez. Özellik için bir DISPROVED tutulduğunda, kural ondan sonra ne gelirse gelsin onu okur; böylece daha sonraki bir PROVED, başka bir modele ait olsa bile bir karşı örneği asla gizlemez: bir modelin özeti, sonucu gönderen kişinin sözüdür. Düzeltilmiş bir modele geçmek için özetini model: içinde belirtin; kural yalnızca o modelin sonuçlarını okur. PROVED, PASS; DISPROVED ise FAIL olur. Diğer her sonuç proof_undecided gerekçesiyle INSUFFICIENT_EVIDENCE, hiç sonuç olmaması ise proof_missing ile INSUFFICIENT_EVIDENCE olur; böylece bir ispatı şart koşan sürüm, ispatı bekler. requires_manual_review: true, sonuç ne olursa olsun girdiyi incelemeye gönderir.

Nerede görünür

oloproof push, bir kapının okuduğu sonuçları taşır. Çalışma alanınız bunları tutar ama bir çözücüyü yeniden çalıştıramaz ya da modelinizi göremez; bu yüzden bir ispatın PASS sonucunu bir kişinin okuması için MANUAL_REVIEW olarak bekletir; bir FAIL veya INSUFFICIENT_EVIDENCE olduğu gibi kalır. Bir karar kaydı, çalıştırmasının kapısının okuduğu sonuçları taşır, ondan sonra içe aktarılan sonuçları değil: record verify her kuralın kararını bunlardan yeniden okur, mühürlendikten sonra düzenlenmiş bir sonucu başarısız sayar ve sonucun kendisini ekibin sözü olarak bildirir.

Sonraki adımlar

• Tehlike kaydı, ters gidebilecek şeyleri anlatır; bir ispat bunları modelde dışlayabilir.
• Gating, bir kuralın sürümü nasıl durdurduğunu anlatır.