Chio/Docs
LOGIN · JOIN

Formal Assurance

Find the machine-checked statement behind an authority rule, the Rust it constrains, and the assumptions your deployment keeps.

Overview chio@5f63e6e

On this page

A formal guarantee is a conjunction: a theorem over a model, a link from that model to the Rust that runs, and the assumptions neither one discharges. Chio states each authority rule that way, so a reviewer can accept or reject every part of it on its own terms.

The rules are the ones an agentic operating system leans on: delegation narrows authority, a revoked capability is refused under its revocation context, and a receipt describes the decision it signs. Formal assurance covers decisions across the platform, from a single kernel to federation, and adds no service to deploy.

Where the formal proof applies, and the audited assumptions each property rests onscope of formal reasoningdeploymentOS, network, tool servers, operatorsRust runtimestores, adapters, transport, I/Odecision coreportable, no_stdproof modelsLean: bounded models andselected core functions1 allowed axiomproofspropertiesaudited assumptions, by classP1P2P3P4P5P6P7P8P9P10cryptography2serialization1platform3storage1transport3external services3external chains1observability1
Where the formal proof applies, and the audited assumptions each property rests onscope of formal reasoningdeploymentOS, network, tool serversRust runtimestores, adapters, I/Odecision coreportable, no_stdproof modelsLean modelspropertiesaudited assumptions, by classP1P2P3P4P5P6P7P8P9P10cryptographyserializationplatformstoragetransportexternal servicesexternal chainsobservability
claim(Pk)  ⇐  proof(Pk) ∧⋀a ∈ A(Pk)a∣A(P4)∣=7\begin{aligned} &\text{claim}(P_k) \;\Leftarrow\; \htmlClass{role-seal}{\text{proof}(P_k)} \,\wedge \bigwedge_{a \,\in\, A(P_k)} \htmlClass{cor-parent}{a} \\ &\lvert A(P_{4}) \rvert = 7 \end{aligned}
P4 · receipt integrity

The registry lists 7 audited assumptions for this property: ED25519, SHA256, CANONICAL-JSON, SQLITE-ATOMICITY, CHAIN-FINALITY, TRACE-OBSERVER, FINDING-STATUS-OPERATOR-COMPLETENESS.

In TOML · assumptions.toml:517 lines
required_assumption_ids = [
  "ASSUME-ED25519",
  "ASSUME-SHA256",
  "ASSUME-CANONICAL-JSON",
  "ASSUME-OS-CLOCK",
  "ASSUME-SQLITE-ATOMICITY",
  "ASSUME-TLS",
  "ASSUME-NETWORK-TRANSPORT",
  "ASSUME-GOSSIP-FAIRNESS-PARTITION-BOUND",
  "ASSUME-EXTERNAL-REGISTRIES",
  "ASSUME-SUBPROCESS-ISOLATION",
  "ASSUME-CHAIN-FINALITY",
  "ASSUME-TRACE-OBSERVER",
  "ASSUME-WASM-ENGINE",
  "ASSUME-FINDING-STATUS-OPERATOR-COMPLETENESS",
  "ASSUME-FINDING-SELLER-TOOL-SERVER",
]
The regions show containment, not size. Properties, classes, and edges come from the audited assumption registry; an edge means the registry lists an assumption of that class for the property. Each property also rests on its proof evidence, which Formal assurance lists by lane.Formal assurance

A claim is read through its statement, its caller, and its assumptions

Three readings, in order, decide whether a guarantee holds for your deployment:

  1. The exact statement. The Theorem Inventory names each property, its domain, and its evidence; a familiar property label does not make every path equally proved.
  2. The production decision. Which Rust helper is extracted or checked, how its caller supplies inputs, and what the caller does when the check refuses.
  3. The external assumptions. Signing, clocks, serialization, durable stores, and remote services keep their own contracts, listed in Assumptions & TCB. A correct scalar check does not establish crash recovery or combined spending conservation.

Verification Evidence compares the methods and explains how to read a source-bound report, and Failure Modes marks where a proof's scope ends.

Each method checks a different object

Lean proofs and extracted-code equivalence, Rust contract verification, bounded exploration, protocol models, and executed tests answer different questions. Lean 4 proves properties of bounded models; the Aeneas pipeline extracts registered Rust and proves it equal to those definitions; Creusot proves contracts on the core; Kani model-checks harnesses within unwind bounds; and TLA+ specifications state protocol invariants that Apalache checks to a stated length.

Executed testing covers what the proofs leave to the implementation. Differential tests compare the reference specification with both Rust scope representations, constant-time tests measure timing on the release builder, fuzz targets run under sanitizers and turn each failure into a regression, mutation testing records how many edits to the trust-boundary crates the suites catch, and the Arena replays scenarios against the kernel and evolves adversary populations against the guards. Research Papers traces each paper's results to the theorems and Rust symbols they rest on.

Delegation cannot widen a grant, and four methods say so differently

In the modeled scope predicate, every child grant needs a covering parent grant, and one uncovered grant rejects the whole proposed scope. An explicit parent invocation cap must stay present in the child and may only narrow: a parent cap of 10 admits a child cap of 4 and rejects 11 or an absent cap.

The extracted Rust predicate optional_u32_cap_is_subset carries a generated-equivalence theorem, so this scalar rule has an implementation link. The broader Lean scope theorem has a different coverage boundary and stops short of full Rust scope refinement, and Kani and the scope comparison check two builds of the Rust comparison. P1: Capability Monotonicity keeps those evidence objects apart and follows the property through all four.

The release you run carries its own proof report

Every release ships with a signed proof report bound to its source commit. The Quickstart checks it for the binary on your PATH with one command and no proof toolchain:

Terminalbash
chio release verify --evidence formal
Output
binary     /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

The command exits 0 only when every line verifies. A report keeps which commands ran, their results, the source revision, and the relevant bounds, and the report contract keeps a coverage inventory apart from a fresh proof run. Maintainers reproduce each lane when qualifying a source revision or changing a decision, as Qualification: formal gates describes.

Next: trace the evidence you need

Work through one propertyFollow capability attenuation across the model and Rust evidence.Find a claimLook up its statement, coverage, and implementation connection.Verify security evidenceCheck signatures, operation bindings, log inclusion, and key history.
PreviousEvidence Capture AuthorityNextVerification Evidence