Assumptions and TCB

Every formal claim is conditioned on a finite set of audited assumptions. Chio names them explicitly in formal/assumptions.toml. The schema is chio.formal-assumptions.v1. This page walks through each row, the rationale chio relies on, and what would happen if the assumption broke.

The Trusted Computing Base

Chio's TCB is intentionally narrow. It is the set of components that, if any of them is wrong, the formal claims do not hold.

• 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

Ten audited assumptions are required by formal/assumptions.toml in required_assumption_ids. Each row below names the ID, the verbatim rationale from the registry, the property IDs the assumption helps discharge, and a note on what would mitigate the assumption breaking in production.

Registry Metadata

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

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

required_assumption_ids = [
  "ASSUME-ED25519",
  "ASSUME-SHA256",
  "ASSUME-CANONICAL-JSON",
  "ASSUME-OS-CLOCK",
  "ASSUME-SQLITE-ATOMICITY",
  "ASSUME-TLS",
  "ASSUME-NETWORK-TRANSPORT",
  "ASSUME-EXTERNAL-REGISTRIES",
  "ASSUME-SUBPROCESS-ISOLATION",
  "ASSUME-CHAIN-FINALITY",
]

Each row in assumptions is a pipe-delimited tuple: ID | category | rationale | discharges. For example, ASSUME-SQLITE-ATOMICITY carries category audited_storage, the rationale verbatim from the table above, and the comma-separated property IDs P2,P4,P6,P7.

CI Artifact: How the Manifest Wires the Registry

The proof manifest at formal/proof-manifest.toml names the registry, the property matrix that consumes the assumptions, and the discharged-assumption list that records every retirement. The gate is cargo test -p chio-formal-diff-tests plus the check-formal-proofs.sh script that reads both files.

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. Audited assumptions appear as named lanes with the form audited_*_assumption:

property_matrix = [
  "P2|presented revocation coverage|lean_root_imported,audited_storage_assumption,sqlite_projection,aeneas_equivalence|proof.revoke_marks_capability_revoked,proof.checkRevocation_revoked_token_errors,...",
  "P4|receipt integrity|lean_root_imported,symbolic_crypto,audited_crypto_assumption,receipt_totality,aeneas_equivalence|proof.membership_proof_sound,proof.receipt_sign_then_verify,...",
  "P8|session continuity soundness|lean_root_imported,audited_transport_assumption,dpop_binding_tests|proof.session_continuity_sound,...",
]

The mapping is direct: audited_storage_assumption in the manifest corresponds to ASSUME-SQLITE-ATOMICITY in the registry; audited_crypto_assumption is ASSUME-ED25519 and ASSUME-SHA256; audited_transport_assumption is ASSUME-TLS and ASSUME-NETWORK-TRANSPORT.

Discharged Assumptions

Discharged assumptions are prior audited assumptions that no longer load-bear. They live in retired_assumptions in the registry and are mirrored in the manifest's discharged_assumptions list. Each one cites the artifacts that took its place.

retired_assumption_ids = [
  "RETIRED-SQLITE-CROSS-ROW",
]

retired_assumptions = [
  "RETIRED-SQLITE-CROSS-ROW|prior_audited_storage|Prior assumption: \
    cross-row SQLite atomicity was assumed for the kernel audit-log \
    append plus the budget-state update happening as a single atomic \
    pair across the receipt-log row and the budget row. This is \
    RETIRED. The kernel relies only on per single-row write atomicity \
    (the surviving ASSUME-SQLITE-ATOMICITY scope) plus the conjunction \
    of the MonotoneLog TLA invariant ... and the per-row budget \
    invariant enforced in crates/chio-kernel/src/budget_store.rs. \
    Together these discharge the cross-row guarantee.|...|P2,P4,P6,P7"
]

The mechanism: a partial-pair crash either leaves an unappended receipt (denied at the next evaluation) or an unupdated budget row (denied by the per-row invariant on the next read). No allow can outrun its log entry without violating one of two named properties, so the prior cross-row assumption was no longer load-bearing.

Worked example: how the discharge lands in the manifest

The retirement of RETIRED-SQLITE-CROSS-ROW is the canonical worked example. Three artifacts changed in lockstep when the assumption was discharged.

Step 1. The original assumption text in formal/assumptions.toml named what was being trusted: that the audit-log append plus the budget-state update happened as an atomic pair across two SQLite rows. The retired row carries the entire prior rationale verbatim plus the discharge artifacts.

retired_assumptions = [
  "RETIRED-SQLITE-CROSS-ROW|prior_audited_storage|Prior assumption: \
    cross-row SQLite atomicity was assumed for the kernel audit-log \
    append plus the budget-state update happening as a single atomic \
    pair across the receipt-log row and the budget row. This is \
    RETIRED. The kernel relies only on per single-row write atomicity \
    (the surviving ASSUME-SQLITE-ATOMICITY scope) plus the conjunction \
    of the MonotoneLog TLA invariant ... and the per-row budget \
    invariant enforced in crates/chio-kernel/src/budget_store.rs. \
    Together these discharge the cross-row guarantee: a partially- \
    applied pair leaves either an unappended receipt (denied at \
    evaluation) or an unupdated budget row (denied by the per-row \
    invariant on the next read), so no allow can outrun its log \
    entry.|MonotoneLog,budget_per_row_invariant|P2,P4,P6,P7"
]

Step 2. The discharge artifact is a TLA+ invariant plus a Rust runtime invariant. The manifest names both, plus the Rust call sites the discharge constrains, in the format id|discharging_artifacts|rust_call_sites|prose.

discharged_assumptions = [
  "RETIRED-SQLITE-CROSS-ROW|\
    MonotoneLog (formal/tla/RevocationPropagation.tla),\
    budget_per_row_invariant (crates/chio-kernel/src/budget_store.rs::BudgetUsageRecord)|\
    crates/chio-kernel/src/receipt_store.rs,\
    crates/chio-kernel/src/budget_store.rs,\
    crates/chio-kernel-core/src/evaluate.rs::evaluate|\
    Cross-row SQLite atomicity for the audit-log append plus \
    budget-state update is no longer assumed. The MonotoneLog TLA \
    invariant proves the per-authority receipt log is append-only and \
    strictly time-monotone, and the per single-row write budget \
    invariant proves BudgetUsageRecord updates are individually \
    atomic and monotone in seq/total_cost. ..."
]

Step 3. The manifest's narrative notes field records the rationale for any human reading the manifest cold:

notes = [
  ...,
  "RETIRED-SQLITE-CROSS-ROW is a discharged assumption: prior \
   cross-row SQLite atomicity is now reduced to per single-row write \
   atomicity (ASSUME-SQLITE-ATOMICITY) plus the MonotoneLog TLA \
   invariant on the audit log and the per-row budget invariant in \
   crates/chio-kernel/src/budget_store.rs. See discharged_assumptions \
   below.",
]

The retirement is therefore a four-file change: the registry, the property matrix that no longer needs the assumption, the manifest's discharged list, and the notes. The check script reads all four and fails if any drift across them.

What Chio Does NOT Trust

Equally important to what is in the TCB: what is not.

• 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.
• Other tenants in a cluster · Multi-tenant clusters share data planes only 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 Narrow Assumptions Matter

Every audited assumption is a footgun the adversary can aim at. A proof that says "capability attenuation holds, assuming ASSUME-ED25519" is a much sharper claim than a proof that says "assuming the signature stack and the storage layer and the canonical-JSON serializer and the OS clock and the network and...".

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. Retired entries stay in the file so historical claims, MAPPING rows, and audit trails remain resolvable. New retirements land via a planning ticket and are mirrored in the proof manifest's discharged_assumptions list.

Release-Facing Claims 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/protocols/STRATEGIC-VISION.md",
  "docs/reference/CLAIM_REGISTRY.md",
  "docs/release/RISK_REGISTER.md",
  "spec/PROTOCOL.md",
]

Any release-facing formal claim in those files must name three things:

• 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 · the assurance pyramid in full.
• Constant-Time Tests · how the timing-channel scope is enforced.
• Trust Model · the broader product framing for what chio trusts and does not.