Assumptions and TCB

The Trusted Computing Base

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

• 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 Report: How the Manifest Uses 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 entry cites the theorem, invariant, or contract that replaced it.

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 \
    ReceiptBeforeAllow Apalache invariant, which states that an allow \
    decision can be recorded only after an allow receipt for the same \
    authority and capability exists in the log. This single invariant \
    replaces the prior joint MonotoneLog plus budget-per-row discharge \
    for the cross-row ordering claim while the budget row remains \
    protected by per-row atomicity.|ReceiptBeforeAllow|P2,P4,P6,P7"
]

ReceiptBeforeAllow is one of the Apalache kernel-state invariants, at formal/apalache/ReceiptBeforeAllow.tla. Receipt persistence and allow publication are separate actions, and the invariant forbids the second without the first: a capability may appear in an authority's allowed set only after an allow receipt for that authority and capability already exists in the log. A partial-pair crash therefore cannot yield an allow that outruns its log entry, so the prior cross-row atomicity assumption no longer limits this claim.

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 registry row in formal/assumptions.toml names 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 discharging theorem or invariant, and it is the source record of the discharge.

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 \
    ReceiptBeforeAllow Apalache invariant, which states that an allow \
    decision can be recorded only after an allow receipt for the same \
    authority and capability exists in the log. This single invariant \
    replaces the prior joint MonotoneLog plus budget-per-row discharge \
    for the cross-row ordering claim while the budget row remains \
    protected by per-row atomicity.|ReceiptBeforeAllow|P2,P4,P6,P7"
]

Step 2. The manifest mirrors the retirement in its discharged_assumptions list, in the format id|discharging_artifacts|rust_call_sites|prose. The registry above records ReceiptBeforeAllow as the discharging invariant; the manifest's mirror still lists the earlier MonotoneLog TLA invariant and the per-row budget invariant. Where the two disagree, the registry in formal/assumptions.toml is the authoritative record.

discharged_assumptions = [
  "RETIRED-SQLITE-CROSS-ROW|\
    MonotoneLog (formal/tla/RevocationPropagation.tla),\
    budget_per_row_invariant (crates/kernel/chio-kernel/src/budget_store.rs::BudgetUsageRecord)|\
    crates/kernel/chio-kernel/src/receipt_store.rs,\
    crates/kernel/chio-kernel/src/budget_store.rs,\
    crates/kernel/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 explanatory 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/kernel/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.

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.

Claim Scope

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

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/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.