Assumptions & TCB

The trusted computing base

Chio's TCB is the set of components whose failure can invalidate a formal claim.

The registry and the list below are not the same set. The registry records what the proofs assume and names an id for each, which is what lets a property cite one. The list is wider: rustc and the hardware under it are trusted without a registry entry, because no proof in the tree is stated in terms of them.

• Cryptographic primitives · The implementations behind ed25519-dalek, sha2, the ecdsa stack for P-256 and P-384, and the canonical-JSON serializer. The proofs treat these symbolically; Chio assumes they satisfy standard unforgeability and collision resistance.
• Rust compiler · The rustc toolchain is trusted to lower the Rust source faithfully. Aeneas extracts a Lean model from the source-level Rust; the binary that actually runs is what rustc produces.
• Operating-system primitives · The OS clock is trusted to deliver operator-accepted Unix time within tolerance. Subprocess isolation and OS process boundaries are trusted for effects outside the kernel. SQLite is trusted for per-row write atomicity.
• Hardware · CPU, memory, and storage are assumed to behave correctly. Chio does not attempt to reason about Rowhammer, voltage glitching, or microarchitectural side channels. The TEE-mode lane (when enabled) reduces the hardware trust set to a specific enclave.
• TLS stack · Endpoint authentication and channel confidentiality on configured remote control and hosted HTTP surfaces.

The assumptions table

required_assumption_ids in formal/assumptions.toml lists 15 ids, and every one of them has a matching row in the assumptions array. scripts/check-formal-proofs.sh compares the two sets and rejects the tree on any difference in either direction, so an id without a statement stops the gate and so does a statement without an id.

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

Each row below carries the id, the statement verbatim from the registry, the property identifiers the row maps to, and a note on what would mitigate the assumption breaking in production. The property column is the row's fourth field: the properties whose evidence rests on the assumption, not properties the assumption discharges. Only the mitigation column is editorial; the other three are rendered from the registry.

Registry metadata

The header of formal/assumptions.toml carries the schema, version, and owner, and the gate scripts/check-formal-proofs.sh rejects any deviation from this shape.

schema = "chio.formal-assumptions.v1"
registry_version = 1
owner = "formal-verification"

Each row in assumptions is a four-field pipe-delimited tuple, and the gate parses the fields as the id, the class, the statement, and the properties the row maps to. It rejects a row with any other arity and a row with an empty field. ASSUME-SQLITE-ATOMICITY carries class audited_storage, the statement shown verbatim in the table above, and P2,P4,P6,P7. The last field says which properties lean on the assumption. Every class name begins audited_: the class says what kind of thing is assumed, not how much it is trusted, and no class means the assumption is discharged.

How the manifest uses the registry

The proof manifest at formal/proof-manifest.toml names the registry in assumption_registry, spends the assumptions as lanes inside property_matrix, and keeps a discharged_assumptions list for retirements. The gate is scripts/check-formal-proofs.sh, which loads both files and rejects a mismatch between them.

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"
claim_registry = "docs/reference/CLAIM_REGISTRY.md"
lean_root_module = "Chio"
boundary_doc = "docs/architecture/CHIO_RUNTIME_BOUNDARIES.md"
spec_anchor = "spec/PROTOCOL.md#55-verified-core-boundary"
primary_toolchain = ["lean4", "creusot", "kani", "aeneas"]

Each row of property_matrix names the lanes that contribute evidence, and an assumption appears there as a lane of the form audited_*_assumption. Six of them occur across the matrix:

Read the lane names as a second vocabulary rather than as ids. The registry sorts its 15 entries into 8 classes (audited_crypto, audited_external, audited_observability, audited_platform, audited_serialization, audited_service, audited_storage, audited_transport), and the manifest's six lane names are not those classes: three of the lanes name a subject the registry has no class for, and five classes name no lane. Nothing in formal/proof-manifest.toml, formal/assumptions.toml or the check script joins one to the other, so a lane on a property row does not resolve to a specific assumption id. To find which assumptions a property rests on, read the P identifiers in the fourth field of each registry row rather than the lane names in the matrix.

Discharged assumptions, of which there are none

A discharged assumption is a prior audited assumption that no longer load-bears, because a proof, an invariant or a contract took over the job. The registry keeps a place for them: retired_assumption_ids and retired_assumptions in formal/assumptions.toml, mirrored by discharged_assumptions in formal/proof-manifest.toml.

All three lists are empty. Every one of the 15 assumptions above is live, and the trusted computing base has not narrowed since the registry was written.

What a proof has to do before an assumption can go

The clearest case is storage. An Apalache invariant, ReceiptBeforeAllow, proves that a receipt is persisted before an allow is published, and a production replay exercises that ordering on the native path. It is a real proof of a real property, and it is the obvious candidate for retiring ASSUME-SQLITE-ATOMICITY.

The manifest declines, in its own words:

ReceiptBeforeAllow proves the abstract persist-before-publish ordering
and its production replay exercises the native happy path. It does not
discharge concrete cross-row crash recovery, which remains excluded until
implementation trace validation and crash-reopen conservation gates
establish refinement.

That is the bar. An abstract model proving an ordering is not the same as the implementation preserving it across a crash, and the gap between them is exactly what an audited assumption is holding. Closing it needs an implementation-refinement gate over the affected production boundary, which the registry says in its own comment above the empty list: abstract invariants and manual mirror hashes are not sufficient by themselves.

The path out is written down and unused. The manifest fixes the shape a retirement takes in the comment above its empty list: a row of id|discharging_artifacts|rust_call_sites|prose citing the retired id in retired_assumptions, the artifacts that discharge it, and the Rust call sites the discharge constrains. Until such a row exists, an assumption that a proof appears to cover is still an assumption.

Components outside the TCB

The following inputs and services are outside the TCB, subject to the stated boundaries.

• Agent input · The agent authoring a tool call is treated as fully untrusted. Every field of every request is parsed and validated before it reaches a verified entrypoint. The fuzz lane covers the parsers; see Fuzz Infrastructure.
• Tool server output · The response from a tool server is treated as untrusted bytes. The kernel decides whether a call is allowed; what the server does with the call, and what it returns, is not part of the proof boundary.
• The network · Beyond the TLS and message-integrity assumptions noted above, the network is treated as actively adversarial. Replay protection, session continuity, and DPoP nonce binding are all proven in the bounded model; the protocol is designed to deny unsafe sequences on the wire. The TLA+ RevocationFreshness invariant constrains only local single-authority revocation-epoch freshness against the model clock; it does not model cross-peer gossip ordering, so ASSUME-NETWORK-TRANSPORT remains audited rather than discharged.
• Other tenants in a cluster · Multi-tenant clusters share data through verified interfaces. A misbehaving tenant cannot widen another tenant's capability by virtue of the structural AttenuationPreserving invariant.
• Hosted registries · Their response is gated on a chio-signed receipt. If a hosted registry lies about state, the receipt log is the source of truth; the registry is advisory.

Side-channel scope

Chio addresses one side channel and explicitly does not address the others.

Why the assumption list stays narrow

A proof that says "capability attenuation holds, assuming ASSUME-ED25519" identifies a smaller dependency set than a proof that assumes the signature stack, storage, canonical-JSON serializer, OS clock, and network together. That is what makes a narrow assumption list worth the bookkeeping.

Two things follow from this principle.

• New assumptions need a written justification. The gate scripts/check-formal-proofs.sh rejects any new entry in required_assumption_ids that lacks a rationale string in assumptions.
• Discharged assumptions are tracked, not deleted. A retired entry stays in the file, in retired_assumption_ids and retired_assumptions, so that historical claims, MAPPING rows, and audit trails stay resolvable. The manifest's discharged_assumptions list mirrors it, and its comment names the format each row must carry: the retired id, the discharging artifacts, the Rust call sites the discharge constrains, and prose.

What a release-facing claim must cite

The manifest's claim_gate_inputs list names the documents whose formal claims are checked against the proof state on every release:

claim_gate_inputs = [
  "README.md",
  "docs/start-here/VISION.md",
  "docs/reference/CLAIM_REGISTRY.md",
  "docs/release/RISK_REGISTER.md",
  "spec/PROTOCOL.md",
]

Each release-facing formal claim in those files must identify its property, model or code, assumptions, boundary, and remaining gap.

• formal/proof-manifest.toml (the manifest the claim is making against)
• formal/theorem-inventory.json (the theorem IDs the claim relies on)
• formal/assumptions.toml (the assumptions the claim is conditioned on)

The script scripts/check-proof-report.sh is the gate that enforces this. A claim that names a theorem which does not appear in the inventory or omits an assumption the theorem requires fails the build.

Next

• Formal Assurance Overview · assurance methods, boundaries, and gaps.
• Constant-Time Tests · how the timing-channel scope is enforced.
• Trust Model · the broader product framing for what Chio trusts and does not.