Dowody formalne

Dowód mówi coś, czego ewaluacja powiedzieć nie może: że własność zachodzi w każdym przypadku modelu, a nie tylko w przypadkach, które zawiera zestaw. Oloproof przechowuje wynik solvera jako materiał dowodowy, a wydanie może go wymagać. Dowód dotyczy sformalizowanego modelu, który zapisałeś, nigdy wdrożenia: dowód, że każdy przelew jest autoryzowany, zachodzi dla modelu uprawnień, a to, czy działający system implementuje ten model, jest osobnym pytaniem, na które odpowiadają twoje zestawy.

Przechowywanie wyniku

Wynik dowolnego solvera trafia do Oloproof według jednego kontraktu, w pliku 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

Rezultat (outcome) to jeden z PROVED, DISPROVED, UNKNOWN, TIMEOUT, ERROR lub NOT_APPLICABLE i jest osobnym polem: nigdy stanem decyzji. certificate i counterexample przechowują to, co dał solver, a timeout_seconds i environment sposób jego uruchomienia. Wynik jest pieczętowany swoją treścią, więc zmieniona kopia jest innym wynikiem. Plik łamiący kontrakt zostaje odrzucony z kodem wyjścia 2, podobnie jak produced_at bez strefy czasowej lub z przyszłości oraz PROVED zawierający kontrprzykład; schemat to schemas/v1/proof_result.schema.json.

Uruchamianie z3

Dla SMT-LIB Oloproof sam uruchamia jeden solver, z3, gdy jest on w twoim PATH (brew install z3, apt install z3 lub pip install z3-solver). Plik zakłada negację własności:

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

unsat oznacza, że w modelu nie istnieje kontrprzykład: PROVED. sat oznacza, że istnieje: DISPROVED, z modelem z3 jako kontrprzykładem, gdy plik o to prosi przez (get-model). unknown to UNKNOWN, przebieg dłuższy niż --timeout to TIMEOUT, a wszystko inne to ERROR: kilka odpowiedzi, błąd po odpowiedzi lub niezerowy kod wyjścia. Jedynym akceptowanym błędem jest komunikat z3, że po unsat żaden model nie jest dostępny, bo nie ma żadnego do podania. oloproof proofs list pokazuje każdy wynik przechowywany przez projekt.

Plik pusty logicznie daje PROVED: gdy własne asercje modelu są ze sobą sprzeczne ((assert false) albo dwa ograniczenia, które nie mogą zachodzić jednocześnie), unsat nie odróżni tego od własności, która zachodzi. Zanim zaufasz dowodowi, sprawdź, że model jest spełnialny bez zanegowanej własności.

Wymaganie dowodu

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

Wpis proofs: w release.yaml jest rozstrzygany przy każdej bramce na podstawie ostatniego otrzymanego wyniku dla jego własności albo dla modelu wskazanego przez model: (skrót), jeśli go ustawisz. Data, którą nosi wynik, niczego nie porządkuje, więc wynik z późniejszą datą nie może ukryć wyniku otrzymanego po nim. Gdy przechowywany jest DISPROVED dla własności, reguła odczytuje go bez względu na to, co nadeszło później, więc późniejszy PROVED nigdy nie ukrywa kontrprzykładu, nawet kontrprzykładu innego modelu: skrót modelu to słowo tego, kto wypchnął wynik. Aby przejść do poprawionego modelu, podaj jego skrót w model:, a reguła odczyta wyłącznie wyniki tego modelu. PROVED to PASS, a DISPROVED to FAIL. Każdy inny rezultat to INSUFFICIENT_EVIDENCE z powodem proof_undecided, a brak jakiegokolwiek wyniku to INSUFFICIENT_EVIDENCE z proof_missing, więc wydanie wymagające dowodu czeka na niego. requires_manual_review: true kieruje go do przeglądu niezależnie od rezultatu.

Gdzie się pojawia

oloproof push przenosi wyniki, które odczytała bramka. Twoja przestrzeń robocza je przechowuje, ale nie może ponownie uruchomić solvera ani zobaczyć twojego modelu, więc wstrzymuje PASS dowodu jako MANUAL_REVIEW, by przeczytał go człowiek; FAIL lub INSUFFICIENT_EVIDENCE pozostaje w mocy. Rekord decyzji zawiera wyniki odczytane przez bramkę jego przebiegu, a nie wyniki zaimportowane później: record verify odczytuje z nich ponownie decyzję każdej reguły, odrzuca wynik zmieniony po zapieczętowaniu i przedstawia sam wynik jako słowo zespołu.

Co dalej

• Rejestr zagrożeń opisuje, co może pójść źle, a dowód może to wykluczyć w modelu.
• Gating opisuje, jak reguła blokuje wydanie.