Formal Assurance Overview

Chio takes a layered approach to assurance. A small pure decision core is proven by hand in Lean 4, refined against Aeneas-extracted Rust, and bounded-model-checked with Kani. A TLA+ specification covers the cross-process revocation propagation protocol that the Lean model cannot reach. Everything outside that proof boundary is held to softer bars: differential property tests, libFuzzer coverage-guided harnesses, dudect timing analysis, and ordinary unit and integration tests. This page is the honest map of which guarantees are which.

Reading Paths by Role

The formal-assurance section is sized for four readers. Pick the path that matches your role; each path is a 30-second scan of which pages to open and what each one gives you.

The Assurance Pyramid

Chio's assurance is layered. The narrowest, strongest layer at the top is hand-written formal proof; the broadest, weakest layer at the bottom is manual review. Each layer is honest about what it can and cannot say.

The general rule: the higher up the table a guarantee lives, the narrower the surface it covers. Mechanized proof reaches the smallest fraction of the codebase but says the strongest things. The bottom layers reach far more code but with weaker guarantees.

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/chio-kernel-core/src/formal_aeneas.rs. See Aeneas Pipeline.
• Kani · Bounded model checker for Rust via CBMC. Symbolically executes proof harnesses on every PR. Public harnesses are at crates/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. The model checker TLC and the bounded type checker Apalache run formal/tla/RevocationPropagation.tla on the PR lane and the nightly liveness lane respectively. 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/chio-kernel-core/tests/dudect/. See Constant-Time Tests.
• libFuzzer + ClusterFuzzLite · Coverage-guided fuzzing across every trust-boundary parser. Targets are in fuzz/fuzz_targets/ with corpora at fuzz/corpus/. See Fuzz Infrastructure.

What Is Formally Verified Today

The proof manifest declares ten required property identifiers, P1 through P10. Each is mapped to a list of Lean theorems plus, in most cases, a Kani harness, an Aeneas equivalence proof, or a Creusot contract.

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. That phrase is doing a lot of work; here is what it means.

The boundary covers the pure security decision surface 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/chio-kernel-core/src/capability_verify.rs",
  "crates/chio-kernel-core/src/scope.rs",
  "crates/chio-kernel-core/src/evaluate.rs",
  "crates/chio-kernel-core/src/formal_aeneas.rs",
  "crates/chio-kernel-core/src/formal_core.rs",
  "crates/chio-kernel-core/src/normalized.rs",
  "crates/chio-kernel-core/src/receipts.rs",
]

Everything outside that list is excluded from the proof boundary. The manifest also names the excluded surfaces verbatim so a reader does not have to infer them: 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 handling; Aeneas extraction from async, IO, SQLite, crypto, and string-heavy production modules outside formal_aeneas.rs; and symlink resolution and OS filesystem root enforcement beyond chio's normalized path-prefix fail-closed checks.

What Is in the Trust Base

Ten audited assumptions remain in formal/assumptions.toml as load-bearing. They are listed by ID; each one names the properties it discharges.

• ASSUME-ED25519 · Ed25519 unforgeability for trusted public keys.
• ASSUME-SHA256 · SHA-256 and Merkle hash collision resistance.
• ASSUME-CANONICAL-JSON · RFC 8785 canonical JSON is deterministic and byte-stable.
• ASSUME-OS-CLOCK · The injected clock reports operator-accepted Unix time within tolerance.
• ASSUME-SQLITE-ATOMICITY · SQLite per-row writes are atomic. Cross-row atomicity is not assumed; that prior assumption is retired.
• ASSUME-TLS · TLS endpoint authentication and channel confidentiality.
• ASSUME-NETWORK-TRANSPORT · Authenticated messages received by chio are not silently rewritten below TLS or signature checks.
• ASSUME-EXTERNAL-REGISTRIES · Hosted package, certification, DID, and registry services return durably accepted state or fail closed.
• ASSUME-SUBPROCESS-ISOLATION · Tool-server subprocess and OS process boundaries hold for effects outside the kernel.
• ASSUME-CHAIN-FINALITY · External chain or oracle finality after the configured confirmation policy accepts the evidence.

See the Assumptions and TCB page for the rationale and mitigation per assumption.

How to Read a Proof Manifest

The manifest at formal/proof-manifest.toml is the canonical proof inventory. Every release-facing formal claim must cite it, the theorem inventory, and the audited assumptions. Here is the shape of the relevant fields.

schema = "chio.proof-manifest.v1"
manifest_version = 1
proof_boundary_status = "implementation_linked_protocol_core"
verification_target = "security_critical_protocol_semantics"
assumption_registry = "formal/assumptions.toml"
primary_toolchain = ["lean4", "creusot", "kani", "aeneas"]

# Root Lean modules. Theorems must be reachable from these to count.
root_modules = [
  "formal/lean4/Chio/Chio.lean",
  "formal/lean4/Chio/Chio/Spec/Properties.lean",
  "formal/lean4/Chio/Chio/Proofs/Monotonicity.lean",
  # ... eight more entries
]

# Gate commands. Run all of these to reproduce the assurance posture.
gate_commands = [
  "./scripts/check-formal-proofs.sh",
  "./scripts/check-aeneas-pilot.sh",
  "./scripts/check-aeneas-production.sh",
  "./scripts/check-aeneas-equivalence.sh",
  "./scripts/check-rust-verification-gates.sh",
  "./scripts/check-kani-public-core.sh",
  "./scripts/check-adapter-no-bypass.sh",
  "cargo test -p chio-formal-diff-tests",
  "./scripts/check-portable-kernel.sh",
  "./scripts/check-proof-report.sh",
]

# Property matrix. Each entry has the form:
#   ID|description|lanes|theorem-ids
# A property is "covered" only when every named lane runs and every
# theorem ID exists in theorem-inventory.json.
property_matrix = [
  "P1|capability attenuation|lean_root_imported,differential_test,...|spec.capability_monotonicity,...",
  # ... nine more rows
]

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

Every gate command in the manifest is a shell script that any contributor can run. The full set of commands reproduces the assurance posture:

# Lean root proofs (sorry-free, root-imported)
./scripts/check-formal-proofs.sh

# Aeneas pilot extraction (formal/aeneas/verified_core.rs)
./scripts/check-aeneas-pilot.sh

# Aeneas production extraction (chio-kernel-core/src/formal_aeneas.rs)
./scripts/check-aeneas-production.sh

# Aeneas-Lean equivalence theorems
./scripts/check-aeneas-equivalence.sh

# Creusot and Kani required-lane verification
./scripts/check-rust-verification-gates.sh

# Public Kani harnesses on chio-kernel-core
./scripts/check-kani-public-core.sh

# Adapter no-bypass: every protocol adapter must call evaluate()
./scripts/check-adapter-no-bypass.sh

# Differential tests: reference spec vs production
cargo test -p chio-formal-diff-tests

# Portable-kernel parity (the same verdict on every target)
./scripts/check-portable-kernel.sh

# Proof report: the final aggregator that all gates fed into
./scripts/check-proof-report.sh

The TLA+ lane is separate, since Apalache is not a Cargo dep. The PR job runs the safety invariants:

# Install Apalache via the pinned tool installer
./tools/install-apalache.sh

# Safety invariants (NoAllowAfterRevoke, MonotoneLog, AttenuationPreserving)
apalache check \
  --inv=SafetyInv \
  --config=formal/tla/MCRevocationPropagation.cfg \
  formal/tla/RevocationPropagation.tla

PASS #11: BoundedChecker
Checker reports no error up to computation length 16
It took me 0 days  3 hours 12 min 47 sec
Total time: 11567.881 sec
EXITCODE: OK

The nightly liveness lane is broader: PROCS=6, CAPS=16, with --temporal=RevocationEventuallySeen gated on the WF_vars(PropagateAny) weak-fairness conjunct in the spec.

What the Proofs Do Not Say

It is worth being explicit about what the assurance layer does not establish.

• The Lean theorems are over bounded models. They do not witness the Rust binary running on a real CPU; they witness mathematical functions written in Lean. The Aeneas equivalence theorems and the Kani and Creusot lanes are what tie the bounded models to executable code.
• Crypto primitives are assumed, not proven. The receipt sign-then-verify theorem is over a symbolic crypto model, not over the Ed25519 implementation in ed25519-dalek.
• Side channels other than timing are out of scope. dudect detects data-dependent timing variation; it does not address power analysis, electromagnetic emanations, or microarchitectural attacks. See the Constant-Time Tests page for what is and is not covered.
• Behavior of tool servers after chio allows a call is out of scope. The receipt records the verdict; what the tool server does next is the operator's concern.
• External chain finality is gated on the configured policy. If your settlement layer reorgs deeper than your finality threshold, the assumption breaks and the receipt evidence does too.

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 its three named safety invariants.
• 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.