Quickstart
Check the formal evidence the release you run carries, read each lane at its scope, and keep the signed report with the claim you cite.
On this page
Every Chio release ships with a strict proof report: Lean, Aeneas, Kani, Creusot, Apalache, the differential suite, and the timing harnesses all ran against the tag's source commit, every gate passed, and the release workflow signed the result. One command checks that report for the binary on your PATH.
A formal claim is only as good as its binding to the code you run. The report ties each lane to one source revision, and the signature ties that revision to the binary you installed, so a property you cite in a review or an audit points at evidence that executed against your release.
StartStrict 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.
1. Check the release you run
Run the verifier with the formal evidence set. It needs the installed chio and network access to the release; the signing identity and the Sigstore trust root are pinned in the CLI.
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
verifiedRead it top down. The first four lines establish that this binary is the published v0.2.0 artifact, signed by the release workflow on backbay-labs/chio, with SLSA provenance for its tag. The formal line establishes that the proof report attached to that tag is bound to the same source commit and records every gate as passed. The indented lines name each lane. The command exits 0 only when every line verifies.
2. Read each lane at its scope
Each lane checks its own object, and a pass carries that object's boundary. Choose the lane from the claim's mapping in the Theorem Inventory: a theorem about a Lean definition, a test of Rust code, and a bounded protocol search answer different questions.
| Lane | Report line | A pass establishes | Its boundary |
|---|---|---|---|
| Scope comparison | diff-tests | The reference specification and both Rust scope representations agree on every generated and fixed case | Differential Tests |
| Lean proofs | lean | Every root-imported theorem builds, no shipped module holds a sorry, and the axiom environment matches the approved list | Lean 4 Proofs |
| Aeneas extraction | aeneas | Fresh extraction of the registered Rust matches the committed snapshots, and the equivalence theorems elaborate | Aeneas Pipeline |
| Kani public core | kani | Every registered PR harness verifies within its unwind bound and input restrictions | Kani Harnesses |
| Creusot contracts | creusot | The core contract obligations prove, and every wrapper delegates to its production twin | Creusot Contracts |
| Apalache models | apalache | Each named invariant holds to its stated length, and every registered broken variant fails | TLA+ Specs |
| Timing | timing | The three dudect harnesses stayed under the threshold on the release builder | Constant-Time Tests |
A pass in one lane leaves the others open. For P1, capability monotonicity, Lean states attenuation over a model of grants, Aeneas ties one scalar rule to extracted Rust, and Kani and the scope comparison check two builds of the Rust comparison. P1: Capability Monotonicity follows that one property through all four.
Two release gates sit beside the formal lanes and answer structural questions: the adapter no-bypass gate checks that every registered adapter routes through the kernel, and the portable-kernel gate builds the core with no default features for the host and for wasm32-unknown-unknown. chio release verify --evidence qualification lists them with every other gate.
3. Keep the report with the claim
A citation outlives the terminal it was checked in. Write the verification as JSON and keep it with the claim, the release tag, and the theorem name:
chio release verify --evidence formal --out proof-evidence-v0.2.0.jsonbinary /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
verified
report ./proof-evidence-v0.2.0.jsonThe JSON carries the binary digest, the signing identity, the provenance subjects, and every gate's recorded result in the manifest's order, so an outside auditor can check the same binding offline. Verification Evidence explains each field of the report.
A binary you built yourself carries no release evidence
The evidence attaches to release artifacts. A chio built from source has no entry in the release's checksum list, so the verifier refuses to apply that release's report to it:
chio release verify --evidence formalbinary /home/ci/.cargo/bin/chio chio 0.2.0 x86_64-unknown-linux-gnu checksum no match in SHA256SUMS for v0.2.0 error[CHIO-RELEASE-PROVENANCE-MISMATCH]: /home/ci/.cargo/bin/chio is not a v0.2.0 release artifact, so no release evidence applies to it help: install the release binary with the published installer, or verify a downloaded archive with chio release verify <ARCHIVE> code: urn:chio:error:release:provenance-mismatch docs: https://chio.computer/docs/reference/errors#error-release-provenance-mismatch
The command exits 1. Install the release binary, or verify the archive you downloaded by path. A maintainer who needs evidence for a source build runs the gates themselves, as Qualification: formal gates describes, and Failure Modes diagnoses a gate that refuses.