Formele bewijzen

Een bewijs zegt iets wat een evaluatie niet kan zeggen: dat een eigenschap geldt in elk geval van een model, niet alleen in de cases die een suite bevat. Oloproof bewaart het resultaat van een solver als bewijsmateriaal, en een release kan er een vereisen. Waar een bewijs over gaat, is het geformaliseerde model dat u hebt opgeschreven, nooit de deployment: een bewijs dat elke overboeking geautoriseerd is, geldt voor het permissiemodel, en of het draaiende systeem dat model implementeert, is een aparte vraag die uw suites beantwoorden.

Een resultaat bewaren

Een resultaat van welke solver ook komt binnen onder één contract, een JSON-bestand:

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

De uitkomst is een van PROVED, DISPROVED, UNKNOWN, TIMEOUT, ERROR of NOT_APPLICABLE, en is een eigen veld: nooit een beslissingstoestand. certificate en counterexample bevatten wat de solver gaf, timeout_seconds en environment hoe hij draaide. Het resultaat wordt verzegeld door zijn inhoud, dus een bewerkte kopie is een ander resultaat. Een bestand dat het contract schendt, wordt geweigerd met exitcode 2, net als een produced_at zonder tijdzone of in de toekomst, en een PROVED met een tegenvoorbeeld; het schema is schemas/v1/proof_result.schema.json.

z3 draaien

Voor SMT-LIB draait Oloproof zelf één solver, z3, wanneer die op uw PATH staat (brew install z3, apt install z3 of pip install z3-solver). Het bestand stelt de ontkenning van de eigenschap:

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

unsat betekent dat er in het model geen tegenvoorbeeld bestaat: PROVED. sat betekent dat er een bestaat: DISPROVED, met het model van z3 als tegenvoorbeeld wanneer het bestand erom vraagt met (get-model). unknown is UNKNOWN, een run voorbij --timeout is TIMEOUT, en al het andere is ERROR: meerdere antwoorden, een fout na het antwoord, of een exitcode die niet nul is. De enige geaccepteerde fout is z3 die na unsat zegt dat er geen model beschikbaar is, omdat er geen te geven is. oloproof proofs list toont elk resultaat dat het project bewaart.

Een vacuüm bestand leest PROVED: wanneer de eigen beweringen van het model elkaar tegenspreken ((assert false), of twee voorwaarden die niet allebei kunnen gelden), kan unsat dat niet onderscheiden van een eigenschap die geldt. Controleer dat het model vervulbaar is zonder de ontkende eigenschap voordat u een bewijs ervan vertrouwt.

Een bewijs vereisen

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

Een proofs:-item in release.yaml wordt bij elke gate beslist op het laatst ontvangen resultaat voor zijn eigenschap, of voor het model dat model: (een digest) noemt wanneer u er een instelt. De datum die een resultaat draagt, bepaalt geen volgorde, dus een later gedateerd resultaat kan er geen verbergen dat daarna werd ontvangen. Wanneer een DISPROVED bewaard is voor de eigenschap, leest de regel dat, wat er ook daarna binnenkwam, dus een latere PROVED verbergt nooit een tegenvoorbeeld, ook niet een van een ander model: de digest van een model is het woord van wie het resultaat pushte. Om over te stappen op een gecorrigeerd model, noem je zijn digest in model:, en de regel leest alleen de resultaten van dat model. PROVED is PASS en DISPROVED is FAIL. Elke andere uitkomst is INSUFFICIENT_EVIDENCE met de reden proof_undecided, en helemaal geen resultaat is INSUFFICIENT_EVIDENCE met proof_missing, dus een release die een bewijs vereist, wacht erop. requires_manual_review: true stuurt het naar beoordeling, wat de uitkomst ook is.

Waar het verschijnt

oloproof push neemt de resultaten mee die een gate las. Uw werkruimte bewaart ze, maar kan geen solver opnieuw draaien en uw model niet zien, dus houdt ze de PASS van een bewijs in als MANUAL_REVIEW, zodat een mens het leest; een FAIL of INSUFFICIENT_EVIDENCE blijft staan. Een beslissingsrecord bevat de resultaten die de gate van zijn run las, niet resultaten die daarna werden geïmporteerd: record verify leest daaruit de beslissing van elke regel opnieuw, laat een resultaat falen dat na het verzegelen werd bewerkt, en vermeldt het resultaat zelf als het woord van het team.

Verder lezen

• Gevarenregister behandelt wat er mis kan gaan, wat een bewijs in het model kan uitsluiten.
• Gating behandelt hoe een regel een release tegenhoudt.