Formal Assurance · Chio Docs

Assurance Methods

Each method examines a different boundary. No method alone establishes every claim:

Method	What it proves
Lean 4	About 83 theorems in a dependently typed logic that state the properties Chio claims.
Aeneas (via Charon)	Extracts Rust into Lean-checkable definitions. Part of the catalog therefore concerns extracted code.
Creusot	Checks function contracts, including preconditions, postconditions, and invariants, against Rust source.
Kani	Bounded model checking searches inputs up to a fixed size for panics, overflows, and assertion failures.
TLA+ with Apalache	Checks safety and liveness in system-level protocol models.
Differential tests	Runs production code and a reference model across many inputs and compares the results.

All six methods use one production file, formal_aeneas.rs. It holds about 15 pure, extraction-safe functions. The functions are executed in production, extracted into Lean by Aeneas and Charon, checked with Creusot contracts, and exercised by Kani harnesses.

rust

// formal_aeneas.rs
// about 15 pure, extraction-safe functions.
// each one is, at the same time:
//   - executed       (the real production code path)
//   - extracted       (Aeneas / Charon -> Lean)
//   - contracted       (Creusot pre/postconditions)
//   - model-checked    (a Kani bounded harness)

The Claim Registry

The methods provide different support for claims. CLAIM_REGISTRY.mdnames ten properties, P1 through P10, maps each property to its supporting method, and states the supported strength of the claim. It also prohibits stronger wording.

Two properties bookend the registry. P1, capability attenuation, is the claim that a delegated capability's authority must narrow relative to its parent. P10, report truthfulness, is the claim that a governed report cannot describe an outcome its receipts do not support. Specific methods support both properties, and the registry specifies permitted wording for each. The registry defines the claims used on this page.

Scope and Limits

Three boundaries limit the proofs. The project documents each boundary so readers can distinguish the proved model from its assumptions and uncovered code paths.

The Signature Is Symbolic

What 'proven' means here

The Lean models of the receipt and Merkle structures use a symbolic signature: inside the model, a signature is the signed body itself. These proofs do not include concrete Ed25519 or SHA-256 inside these proofs. Concrete cryptographic soundness is instead an audited assumption, named explicitly (ASSUME-ED25519, ASSUME-SHA256) and reviewed as an assumption, not a theorem. For that reason, the receipts are formally verified end to end is a phrasing the claim registry forbids: the receipt structure is verified end to end; the signature remains a trusted assumption.

The assumptions register records both assumptions with the other trusted-computing-base assumptions on which the proofs depend.

A Model, Not the Whole Codebase

Most of the catalog, about 69 of roughly 83 theorems, is proved over a bounded, hand-written protocol model, not directly over production Rust. Two checks link the model to Rust: a mechanical symbol-existence check confirms the Rust functions the model claims to describe still exist with matching signatures, and a smaller set, about 14, of hand-proved equivalence theorems show that specific model functions behave the same as their Rust counterparts. This does not establish functional equivalence between the model and the entire codebase.

Coverage Is Uneven

The verification methods do not all run at the same rate. Kani, Lean, and mutation testing run nightly rather than on each pull request. Differential tests run on each PR. A regression caught by a nightly method can remain on the main branch for up to a day. Most verified helper functions are proved about their model counterparts and are not called in production. The time-window classifier and NormalizedToolGrant::is_subset_ofare among the exceptions. Elsewhere, verified describes the model counterpart.

Thin coverage for request teardown

The drop and cancel-unwind path runs when a request is torn down mid-flight. It has caused kernel bugs and has the thinnest formal coverage in the system. The mutation-testing kill rate for these methods is about 30 percent, below the 80 percent target. A mutated implementation can therefore escape these checks.

These limits define the support for claims on this page. The registry distinguishes proved claims, assumptions, model coverage, and uncovered production paths.

Summary

Assurance methods. Lean 4, Aeneas, Creusot, Kani, TLA+ with Apalache, and differential tests use formal_aeneas.rs.
Claim registry. CLAIM_REGISTRY.md maps P1 through P10 to their supporting method and prohibits stronger wording.
Signature assumptions. Ed25519 and SHA-256 soundness are documented assumptions (ASSUME-ED25519, ASSUME-SHA256), not theorems.
Bounded model coverage. About 69 of 83 theorems hold over a bounded model, linked to Rust by a symbol check and about 14 equivalence theorems, not full functional equivalence.
Uneven coverage. Verification methods run nightly, differential tests run on each PR, the drop/cancel-unwind path has thin coverage, and the mutation-testing kill rate is below target.

Next Steps

Verifiable Evidence · what a receipt has to contain before it counts as evidence at all
Trust Boundaries & Limits · the parts of the system proofs do not reach, stated in one place
Trust Model · the zero-ambient-authority stance the claim registry is scoped inside
Formal Overview · the full lane-by-lane tour of the verification stack
Theorem Inventory · the actual list behind the roughly-83 figure on this page
Assumptions & TCB · every named assumption the proofs stand on, including ASSUME-ED25519 and ASSUME-SHA256

PreviousVerifiable Evidence NextTrust Boundaries & Limits