Prove formali

Una prova dice qualcosa che una valutazione non può dire: che una proprietà vale in ogni caso di un modello, non solo nei casi contenuti in una suite. Oloproof conserva il risultato di un solver come evidenza, e un rilascio può richiederne uno. Ciò su cui verte una prova è il modello formalizzato che avete scritto, mai il deployment: una prova che ogni trasferimento è autorizzato vale per il modello dei permessi, e se il sistema in esecuzione implementa quel modello è una domanda separata, a cui rispondono le vostre suite.

Conservare un risultato

Il risultato di qualsiasi solver entra sotto un unico contratto, un 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

L'esito è uno tra PROVED, DISPROVED, UNKNOWN, TIMEOUT, ERROR o NOT_APPLICABLE, ed è un campo a sé: mai uno stato di decisione. certificate e counterexample contengono ciò che il solver ha fornito, timeout_seconds e environment come è stato eseguito. Il risultato è sigillato dal suo contenuto, quindi una copia modificata è un risultato diverso. Un file che viola il contratto viene rifiutato con codice di uscita 2, e così un produced_at senza fuso orario o nel futuro, e un PROVED che porta un controesempio; lo schema è schemas/v1/proof_result.schema.json.

Eseguire z3

Per SMT-LIB, Oloproof esegue da sé un solo solver, z3, quando si trova nel vostro PATH (brew install z3, apt install z3 o pip install z3-solver). Il file asserisce la negazione della proprietà:

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

unsat significa che nel modello non esiste alcun controesempio: PROVED. sat significa che ne esiste uno: DISPROVED, con il modello di z3 come controesempio quando il file lo chiede con (get-model). unknown è UNKNOWN, un'esecuzione che supera --timeout è TIMEOUT, e qualsiasi altra cosa è ERROR: più risposte, un errore dopo la risposta o un'uscita diversa da zero. L'unico errore accettato è z3 che dice che nessun modello è disponibile dopo unsat, poiché non ce n'è alcuno da dare. oloproof proofs list mostra ogni risultato conservato dal progetto.

Un file vacuo risulta PROVED: quando le asserzioni stesse del modello si contraddicono ((assert false), o due vincoli che non possono valere insieme), unsat non può distinguerlo da una proprietà che vale. Verificate che il modello sia soddisfacibile senza la proprietà negata prima di fidarvi di una sua prova.

Richiedere una prova

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

Una voce proofs: in release.yaml viene decisa a ogni gate sull'ultimo risultato ricevuto per la sua proprietà, o per il modello indicato da model: (un digest) quando lo impostate. La data che un risultato porta non ordina nulla, quindi un risultato datato più tardi non può nasconderne uno ricevuto dopo. Quando è conservato un DISPROVED per la proprietà, la regola legge quello, qualunque cosa sia arrivata dopo, quindi un PROVED successivo non nasconde mai un controesempio, nemmeno di un altro modello: il digest di un modello è la parola di chi ha inviato il risultato. Per passare a un modello corretto, indica il suo digest in model: e la regola legge solo i risultati di quel modello. PROVED è PASS e DISPROVED è FAIL. Qualsiasi altro esito è INSUFFICIENT_EVIDENCE con il motivo proof_undecided, e l'assenza di qualsiasi risultato è INSUFFICIENT_EVIDENCE con proof_missing, quindi un rilascio che richiede una prova la aspetta. requires_manual_review: true la manda in revisione qualunque sia l'esito.

Dove compare

oloproof push porta i risultati letti da un gate. Il vostro spazio di lavoro li conserva ma non può rieseguire un solver né vedere il vostro modello, quindi trattiene il PASS di una prova come MANUAL_REVIEW perché lo legga una persona; un FAIL o un INSUFFICIENT_EVIDENCE resta valido. Un record di decisione porta i risultati letti dal gate della sua esecuzione, non i risultati importati dopo: record verify rilegge da essi la decisione di ogni regola, fa fallire un risultato modificato dopo essere stato sigillato e riporta il risultato stesso come parola del team.

Dove andare dopo

• Registro dei pericoli tratta ciò che può andare storto, che una prova può escludere nel modello.
• Gating tratta come una regola blocca un rilascio.