Preuves formelles

Une preuve dit ce qu’une évaluation ne peut pas dire : qu’une propriété tient dans chaque cas d’un modèle, et pas seulement dans les cas que contient une suite. Oloproof conserve le résultat d’un solveur comme preuve, et une publication peut en exiger un. Une preuve porte sur le modèle formalisé que vous avez écrit, jamais sur le déploiement : une preuve que chaque virement est autorisé tient pour le modèle de permissions, et savoir si le système en production implémente ce modèle est une question distincte, à laquelle vos suites répondent.

Conserver un résultat

Le résultat de n’importe quel solveur entre sous un seul contrat, un fichier 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’issue est l’une de PROVED, DISPROVED, UNKNOWN, TIMEOUT, ERROR ou NOT_APPLICABLE, et c’est un champ à part : jamais un état de décision. certificate et counterexample contiennent ce que le solveur a fourni, timeout_seconds et environment la façon dont il a tourné. Le résultat est scellé par son contenu, si bien qu’une copie modifiée est un autre résultat. Un fichier qui enfreint le contrat est refusé avec le code de sortie 2, de même qu’un produced_at sans fuseau horaire ou situé dans le futur, et qu’un PROVED qui porte un contre-exemple ; le schéma est schemas/v1/proof_result.schema.json.

Exécuter z3

Pour SMT-LIB, Oloproof exécute lui-même un solveur, z3, quand il est dans votre PATH (brew install z3, apt install z3 ou pip install z3-solver). Le fichier affirme la négation de la propriété :

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

unsat signifie qu’aucun contre-exemple n’existe dans le modèle : PROVED. sat signifie qu’il en existe un : DISPROVED, avec le modèle de z3 comme contre-exemple quand le fichier le demande avec (get-model). unknown donne UNKNOWN, une exécution qui dépasse --timeout donne TIMEOUT, et tout le reste donne ERROR : plusieurs réponses, une erreur après la réponse, ou un code de sortie non nul. La seule erreur acceptée est z3 disant qu’aucun modèle n’est disponible après unsat, puisqu’il n’y en a aucun à fournir. oloproof proofs list montre chaque résultat que le projet détient.

Un fichier vide de sens donne PROVED : lorsque les assertions du modèle lui-même se contredisent ((assert false), ou deux contraintes qui ne peuvent tenir ensemble), unsat ne peut pas distinguer ce cas d’une propriété qui tient. Vérifiez que le modèle est satisfiable sans la propriété niée avant de vous fier à une preuve de celle-ci.

Exiger une preuve

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

Une entrée proofs: dans release.yaml est décidée à chaque porte sur le dernier résultat reçu pour sa propriété, ou pour le modèle nommé par model: (un condensé) quand vous en fixez un. La date que porte un résultat n’ordonne rien, si bien qu’un résultat daté plus tard ne peut pas masquer un résultat reçu après lui. Lorsqu’un DISPROVED est détenu pour la propriété, la règle le lit quoi qu’il soit arrivé ensuite, si bien qu’un PROVED ultérieur ne masque jamais un contre-exemple, même celui d’un autre modèle : le condensé d’un modèle est la parole de qui a poussé le résultat. Pour passer à un modèle corrigé, nommez son condensé dans model:, et la règle lit les résultats de ce seul modèle. PROVED donne PASS et DISPROVED donne FAIL. Toute autre issue donne INSUFFICIENT_EVIDENCE avec la raison proof_undecided, et l’absence de tout résultat donne INSUFFICIENT_EVIDENCE avec proof_missing : une publication qui exige une preuve l’attend. requires_manual_review: true l’envoie en revue quelle que soit l’issue.

Où elle apparaît

oloproof push porte les résultats qu’une porte a lus. Votre espace de travail les détient mais ne peut ni relancer un solveur ni voir votre modèle, il retient donc le PASS d’une preuve comme MANUAL_REVIEW pour qu’une personne le lise ; un FAIL ou un INSUFFICIENT_EVIDENCE reste tel quel. Un enregistrement de décision porte les résultats que la porte de son exécution a lus, pas des résultats importés après elle : record verify relit la décision de chaque règle à partir d’eux, fait échouer un résultat modifié après avoir été scellé, et présente le résultat lui-même comme la parole de l’équipe.

Pour aller plus loin

• Registre des dangers couvre ce qui peut mal tourner, qu’une preuve peut exclure dans le modèle.
• Gating couvre la façon dont une règle bloque une publication.