Formal Assurance Overview

Reading paths by role

These four paths group the pages by reader role. Each path identifies the pages to open and the information they provide.

Methods and what each one claims

These methods differ in target, model, and assurance claim, and the manifest does not rank them against each other. It records each Rust lane as a lane|posture|path row in rust_refinement_lanes. The 5 rows there register Creusot once, Kani once for each of its two harness registries, and Aeneas at both pilot and production. The manifest notes say what those standings mean: Creusot and Kani are required strict-CI lanes for production implementation linkage, while Lean assets count as release evidence only when they are root-imported, free of sorry, and mapped to a property_matrix entry. Read each row below for its own coverage and its own claim.

Mechanized proofs cover smaller models than tests and review. The distinction is stated in each row's coverage and claim.

The tools Chio uses

• Lean 4 · Proof assistant for the capability algebra, revocation snapshots, evaluation totality, receipt coupling, and protocol-level closure theorems. Source under formal/lean4/Chio/. See Lean 4 Proofs.
• Aeneas · Extracts a functional model from Rust source for proving in Lean (the original Aeneas pipeline targets F*; Chio extracts to Lean instead, paired with explicit equivalence theorems). Two lanes: a pilot at formal/aeneas/verified_core.rs and the production extraction from crates/kernel/chio-kernel-core/src/formal_aeneas.rs. See Aeneas Pipeline.
• Kani · Bounded model checker for Rust via CBMC. Symbolically executes the public proof harnesses in the nightly kani-public-nightly lane. Public harnesses are at crates/kernel/chio-kernel-core/src/kani_public_harnesses.rs. See Kani Harnesses.
• Creusot · SMT-backed refinement-type prover that pins contracts to production Rust symbols. Configured in formal/rust-verification/creusot-contracts.toml.
• TLA+ · Temporal-logic spec language. Apalache checks the safety invariants of formal/tla/RevocationPropagation.tla on the path-scoped PR lane and its liveness property on a nightly lane. The same PR lane covers formal/tla/DelegationDepthBound.tla, formal/tla/DistributedRevocation.tla under two configs, and the kernel-state specs under formal/apalache/: MonotoneLogApalache, RevocationCutCompleteness, ReceiptBeforeAllow, KernelTransitionCancelSafe, and PostAdmissionDropGuard. See TLA+ Specs.
• proptest · Property-based generator for differential tests in formal/diff-tests/. See Differential Tests.
• dudect · Statistical detector for data-dependent timing in tight inner loops. Lives in crates/kernel/chio-kernel-core/tests/dudect/. See Constant-Time Tests.
• libFuzzer + ClusterFuzzLite · Coverage-guided fuzzing across the trust-boundary parsers listed in the target directory. Targets are in fuzz/fuzz_targets/ with corpora at fuzz/corpus/. See Fuzz Infrastructure.
• cargo-mutants · Mutation testing across six trust-boundary crates (chio-policy, chio-credentials, chio-attest-verify, chio-kernel-core, chio-guards, chio-anchor). Runs nightly as an advisory lane, with a co-coverage job that replays the fuzz corpus against surviving mutants. Configured in .github/workflows/mutants.yml.

What the manifest claims today

required_property_ids declares 10 identifiers, P1 through P10, and property_matrix gives each one a description, a list of evidence lanes, and the theorem ids that stand behind it. The lane column here is that list verbatim; a lane named audited_* is an assumption the property rests on rather than a check that runs.

For the full per-theorem table, see the Theorem Inventory.

The proof boundary

The manifest names the boundary explicitly: implementation_linked_protocol_core. The verification target is security_critical_protocol_semantics.

The boundary covers the pure security-decision code inside chio-kernel-core plus bounded models of adjacent state transitions (revocation snapshots, budget commits, DPoP nonce admission, guard pipeline composition, receipt coupling). The covered Rust modules listed in the manifest are:

covered_rust_modules = [
  "crates/kernel/chio-kernel-core/src/capability_verify.rs",
  "crates/kernel/chio-kernel-core/src/scope.rs",
  "crates/kernel/chio-kernel-core/src/evaluate.rs",
  "crates/kernel/chio-kernel-core/src/formal_aeneas.rs",
  "crates/kernel/chio-kernel-core/src/formal_core.rs",
  "crates/kernel/chio-kernel-core/src/normalized.rs",
  "crates/kernel/chio-kernel-core/src/receipts.rs",
  "crates/core/chio-core-types/src/merkle.rs",
  "crates/core/chio-core-types/src/merkle_steps.rs",
  "crates/economy/chio-credit/src/formal_economy.rs",
  "crates/economy/chio-web3/src/settlement.rs",
  "crates/trust/chio-federation/src/revocation_gossip.rs",
  "crates/economy/chio-open-market/src/finding_slash_amount.rs",
]

That list is not the whole of what carries verification evidence. The manifest keeps a second list, covered_rust_symbols, and the two disagree: 47 symbols sit in 17 distinct module paths, and 4 of those paths never appear in covered_rust_modules at all (chio_core_types::capability, chio_core_types::delegation_receipt, chio_kernel_core::revocation_view, chio_revocation_oracle::api). Read the module list as the declared file set rather than as a boundary, and check the symbol list before concluding that a module is uncovered.

What is outside the boundary the manifest states directly, in excluded_surfaces: concrete Ed25519, SHA-256, canonical JSON, TLS, OS clock, SQLite, chain, and hosted-registry implementations beyond their audited assumptions; async scheduling, network delivery, subprocess effects, and tool-server behavior after the verified decision core allows a call; cluster consensus, external settlement rails, and third-party registry availability beyond fail-closed Chio handling; Aeneas extraction from async, IO, SQLite, crypto, and string-heavy production modules outside the registered sources in formal/aeneas/production.toml; reservation-ledger refinement from the pure ledger_apply model to concrete BudgetStore mutations; symlink resolution and OS filesystem root enforcement beyond Chio's normalized path-prefix fail-closed checks; cross-row receipt and budget crash recovery, ordering, and conservation; runtime trace callbacks omitted or rewritten before delivery to the installed observer; Treaty PredicateLang parsing, hashing, signature verification, store lookup, and completeness outside its explicit AdmissionView decision domain; float-valued JSON leaves in compound receipt-ID fields; refinement from the mechanized canonical projection to crates/core/chio-core-types/src/canonical.rs beyond the checked integer-domain fixtures and differential tests; and wasmtime interpreter, compiler, JIT, sandbox, and host-import information-flow behavior beyond Chio's typed verdict dispatch.

Scope and gaps

The receipt theorems prove properties over a symbolic cryptography model, under the Ed25519 and SHA-256 assumptions recorded in formal/assumptions.toml, rather than concrete cryptographic implementations. Most catalog entries prove bounded models, not the running binary. Kani and Lean run nightly, not on each pull request. The drop and cancel-unwind path, which runs when a request is torn down mid-flight, is covered by formal/apalache/PostAdmissionDropGuard.tla at the bound the manifest states: two invocations and one buffered child per invocation, with evidence requiring both a positive NoError result and every paired negative mutation producing a registered ITF counterexample. See Formal Assurance for the full honest-scope treatment.

How to read the proof manifest

The manifest at formal/proof-manifest.toml is the proof inventory. Each release-facing formal claim must cite it, the theorem inventory, and the audited assumptions. Its header pins the schema and the boundary: chio.proof-manifest.v1, implementation_linked_protocol_core, security_critical_protocol_semantics, and primary_toolchain = ["lean4", "creusot", "kani", "aeneas"].

Four arrays carry the substance. root_modules names the 37 Lean modules a theorem must be reachable from to count, listed in full on the Lean 4 Proofs page. property_matrix holds one ID|description|lanes|theorem-ids row for each of the 10 required properties. covered_rust_modules and covered_rust_symbols are the two file and symbol lists above. And gate_commands is the set of commands that reproduces every result the manifest records:

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",
]

Three rules govern the manifest:

• A theorem only counts as evidence if it is root-imported from the modules in root_modules and contains no sorry.
• A property only counts as covered if every lane in its property matrix entry runs green in CI.
• Excluded surfaces and audited assumptions must be cited explicitly. Silent assumptions are forbidden.

Reproducing the proofs locally

gate_commands above is the list, in the order the manifest keeps it. Each entry is a shell script or a cargo invocation a contributor runs from the repository root, and the lanes they drive are the Lean root proofs, the Aeneas pilot and production extractions and their equivalence theorems, the Creusot and Kani required lanes, the public Kani core lane, the manual-mirror hash check, adapter no-bypass, the differential tests, portable-kernel parity, the receipt-trace and distributed-revocation refinement checks, and the proof-report aggregator that consumes the rest.

Two of them need nothing beyond a Rust toolchain and a shell, so they are the ones to run first against a clone. ./scripts/check-adapter-no-bypass.sh is a four-line wrapper that execs cargo xtask check adapter-no-bypass; on success that command prints adapter-no-bypass: structured mediation contracts passed from xtask/src/adapter_no_bypass.rs. cargo test -p chio-formal-diff-tests compiles the crate library plus the test files in formal/diff-tests/tests/, which cover anchored roots and their tamper cases, canonical JSON in both the native and browser encoders, receipt encoding, scope subsumption, treaty predicates, and one named regression pinned to the ReceiptBeforeAllow lane.

Two of the cases in receipt_encoding_diff.rs carry #[ignore]. They spawn python3 and node subprocesses against the live Python and TypeScript SDKs, and they opt in through CHIO_LIVE_SDK_DIFFERENTIAL=1 cargo test -- --ignored rather than failing when the SDK is absent.

The TLA+ lane is separate, since Apalache is not a Cargo dependency. ./tools/install-apalache.sh installs the pinned checker, and ./scripts/check-apalache-positive.sh drives one spec at one bound, taking --invariant, --length, --timeout-seconds and --config alongside the spec path. The pull-request job in .github/workflows/apalache-safety.yml runs it once per matrix shard, and the shard covering formal/tla/RevocationPropagation.tla passes SafetyInv at length: 6 with timeout_seconds: 10800. The other shards cover the specs under formal/apalache/, formal/tla/DistributedRevocation.tla under two configs and two different invariants, and formal/tla/DelegationDepthBound.tla.

The nightly liveness lane holds the same PROCS=4, CAPS=8 bounds as the PR safety run but drives them to a deeper computation length (--length=24) with --temporal=RevocationEventuallySeen gated on the WF_vars(PropagateAny) weak-fairness conjunct in the spec. It is a scheduled lane, not a required PR gate.

Next steps

• Theorem Inventory · the full table of theorems by ID, statement, tool, file, and status.
• Assumptions and TCB · what Chio trusts, why, and what would mitigate each assumption breaking.
• Aeneas Pipeline · how the production extraction is wired to the Lean equivalence theorems.
• Lean 4 Proofs · the proof structure, file by file.
• Kani Harnesses · the public harness inventory plus per-harness wall clocks.
• TLA+ Specs · the revocation-propagation spec and the invariants it names.
• Differential Tests · reference spec vs production for the surfaces that proofs do not cover.
• Constant-Time Tests · dudect harnesses and how to read their output.
• Fuzz Infrastructure · the trust-boundary fuzz target inventory.

For the broader trust framing, the Trust Model page explains where formal assurance sits inside Chio's zero-ambient-authority design.