Verification Evidence
Trace a formal property to its statement, its assumptions, and recorded gate results, and tell an executed proof run from a coverage catalog.
On this page
A Chio proof report records which verification commands ran, against which source revision, and with what result, so a cited property traces to evidence that executed.
Each property maps through the proof manifest to named statements, the assumptions they rely on, and the gates that check them. Lean, Aeneas, Creusot, Kani, Apalache, differential tests, fuzzing, and timing analysis each reason about their own object, and the report keeps their results apart.
Strict mode runs every registered gate
The coverage preflight joins the manifest, inventory, and registry. Strict mode then runs the registered commands and captures each exit and status, and the checker requires every recorded gate to have passed.
The report keeps a coverage catalog apart from a proof run
The report generator joins the declared inventory with source identities and gate results. In strict mode it runs every registered command and captures each exit and status. In metadata_only mode it runs the coverage preflight and records the remaining gates with status not_run.
The report checker validates an existing report's structure and its binding to source, reading the recorded results without replaying the proof commands. It requires gate results in the manifest's exact order, after excluding the generator and checker commands themselves. Strict mode requires every recorded gate to have passed, and a release accepts only a strict report: a metadata_only report never ships.
A release-facing claim also keeps the wording and scope recorded in the claim registry.
The registered commands
gate_commands = [
"cargo xtask gen proof-coverage --check",
"./scripts/check-formal-proofs.sh",
"./scripts/check-aeneas-pilot.sh",
"./scripts/check-aeneas-production.sh",
"./scripts/check-aeneas-equivalence.sh",
"./scripts/tests/aeneas-equivalence.test.sh",
"./scripts/check-rust-verification-gates.sh",
"cargo xtask check formal-mirrors",
"./scripts/check-kani-public-core.sh",
"./scripts/run-kani-manifest.sh --lane pr --crate chio-open-market",
"./scripts/check-adapter-no-bypass.sh",
"cargo test -p chio-formal-diff-tests",
"./scripts/check-portable-kernel.sh",
"./scripts/check-receipt-trace.sh",
"./scripts/check-distributed-revocation-refinement.sh",
"./scripts/check-proof-report.sh",
]Ten properties reach named statements through three records
The property matrix groups claims under P1 to P10: attenuation, presented revocation, fail-closed evaluation, receipt integrity, delegation structure, local parent links, receipt lineage, session continuity, provenance consistency, and report truthfulness. Each surface under a property carries its own evidence, so read the entry for the surface you cite. Three records define that scope:
- Proof manifest. The properties, symbols, evidence lanes, commands, and exclusions Chio declares.
- Theorem inventory. The statement and declaration behind each cited property, searchable with its mapped property and declared source in the Theorem Inventory.
- Assumption registry. The external contract each mapped property depends on, with its operational consequences in Assumptions & TCB.
The manifest also lists the covered Rust modules and symbols, and the generated coverage join navigates from a surface to its declared evidence. Coverage is declared per symbol: a listed module can still hold functions, callers, and effects that no formal method checks.
A proved helper decides inside the runtime path
The implementation-linked core places pure security decisions inside the running kernel. Registered budget, DPoP, nonce-replay, guard, revocation, and receipt-coupling paths project their inputs into those helpers, and the helper must approve before the continuation or signing step runs.
Relying on one means reading three things: the helper's property, the caller's projection of its inputs, and the caller's response to a refusal. A theorem about a boolean helper covers the helper; whether each caller supplied the correct boolean belongs to the caller's evidence. The P1 tour follows capability attenuation this way, and receipt coupling connects a live call path to a decision helper that gates a signed result.
Signing and hashing, production serialization, clocks, durable state, sandbox engines, and remote services rely on the evidence or assumptions named for those boundaries. Cross-row crash recovery and unobserved tool effects sit outside any pure decision proof; Trust Boundaries & Limits connects those obligations to the running system.
Each method checks its own object
Cite a result together with the boundary it carries.
| Method | Evidence it produces | Boundary to keep |
|---|---|---|
| Lean 4 | Machine-checked statements over declared models, with an axiom inventory | The theorem's inputs, assumptions, and modeled domain |
| Charon and Aeneas | Lean extracted from registered Rust, with equivalence theorems to the models | Extraction, snapshot agreement, and elaboration are separate checks; compiled instructions stay outside |
| Creusot | Proof obligations for registered Rust contracts, with body-synchronization checks | Each contract needs its implementation link and a passing lane; a file hash alone is insufficient |
| Kani | Symbolic harness results over registered inputs, assumptions, and unwind settings | The harness bounds and its unwinding-check policy |
| TLA+ and Apalache | Named invariants or temporal properties under one model configuration | Finite bounds, fairness, and partition assumptions |
| Differential tests | An executable specification compared with production behavior on generated inputs | A passing sample; keep and replay any counterexample |
| Fuzzing and timing analysis | Adversarial inputs and measured timing differences on registered harnesses | Coverage and measurement conditions; a clean run is a sample |
Two methods mapped to one property still reason about different objects. For P1, Lean states attenuation over a model of grants, while Kani explores a bounded build of the Rust comparison, so each result is cited at its own boundary.
Every release carries a strict report
The release workflow generates a strict report before it tags a release, checks it, signs it, and attaches it bound to the tag's source commit. chio release verify checks that signature and binding for the binary you run and prints each lane's result. --out keeps the verification report as JSON, so the evidence you cite travels with the claim.
chio release verify --evidence formalbinary /usr/local/bin/chio chio 0.2.0 aarch64-apple-darwin
checksum matches SHA256SUMS for v0.2.0
signed by release.yml on backbay-labs/chio, issuer token.actions.githubusercontent.com
provenance SLSA v1, 5 subjects, tag v0.2.0
formal proof report bound to v0.2.0, every gate passed
lean root-imported theorems checked
aeneas production extraction and equivalence
kani public PR lane
apalache positive and negative invariants
creusot core contracts
diff-tests scope, canonical JSON, receipts, treaties
timing dudect threshold
verifiedKeep that JSON with the claim, the release tag, and the property's entry in the Theorem Inventory: chio release verify --evidence formal --out proof-evidence.json. Maintainers generate and check the report from source, with the pinned toolchains, as described in Qualification: formal gates.
When a stage refuses, Failure Modes separates a counterexample from missing or inconsistent evidence and names the next diagnostic.