Assumptions & TCB

Trusted computing base

A trusted computing base is the set of components and contracts whose failure can invalidate the guarantee you rely on. Which components belong to it depends on the claim: a pure decision theorem rests on its model and proof assumptions, and the executing kernel adds compilation, input projection, platform services, and the effects outside the pure core.

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

Four boundaries sit between a proof and a running deployment, from the model outward:

1. Mechanized model. Inspect the theorem statement, imported declarations, and explicit Lean axioms. The manifest and theorem inventory name the accepted formal surface, and the Lean environment audit checks its axiom and opaque declarations.
2. Production connection. Inspect which runtime caller invokes the helper, how it constructs inputs, and how a refusal affects continuation. The registry declares implementation links and evidence lanes, each with its own verification boundary.
3. External contract. Inspect the signer, serializer, clock, store, transport, sandbox, or service. The registry names the assumption and its mapped properties; the external implementation carries its own verification.
4. Executing platform. Inspect the compiler, binary, operating system, hardware, and deployment configuration. The external-assumption list names the contracts the proofs cite, and the deployed trusted computing base is larger than that list.

Assumption classes

The registry groups contracts as crypto, serialization, platform, storage, transport, service, external, and observability assumptions. A class describes the kind of dependency and carries no trust grade: a proof that cites a transport contract is conditional on that contract, as one citing a cryptographic contract is conditional on its primitive.

Assumption entries

Each entry gives the registry identifier, class, mapped property identifiers, and exact statement, then an operating note. The Theorem Inventory holds the statements behind P1 through P10.

Signing and verification

ASSUME-ED25519 · audited_crypto · Properties P2, P3, P4

Ed25519 verification and signing are assumed to satisfy standard unforgeability for trusted public keys.

If the contract fails. Determine whether the failure concerns a compromised key, an implementation defect or the primitive itself. Suspend reliance on affected signatures until the relevant trust or protocol change is reviewed. Key rotation alone cannot repair a broken cryptographic primitive.

Receipt and checkpoint hashes

ASSUME-SHA256 · audited_crypto · Properties P4, P7

SHA-256 and Merkle hash collision resistance are assumed for concrete receipt and checkpoint evidence.

If the contract fails. Preserve the original artifacts and reassess which digest-based links remain trustworthy. A replacement hash scheme needs an explicit compatibility and evidence plan; re-anchoring an old digest does not repair the evidence that digest already failed to bind.

Canonical signed bytes

ASSUME-CANONICAL-JSON · audited_serialization · Properties P4, P7, P10

The production canonicalizer is assumed to agree byte-for-byte with the mechanized UTF-8 renderer on Unicode scalar strings, normalized bounded integers, arbitrary finite arrays, and UTF-16-ordered objects. Float rendering and float-bearing compound receipt fields outside that domain remain assumed deterministic and byte-stable.

If the contract fails. Keep the original payload bytes, serializer version and conflicting encodings. Reproduce the disagreement against the canonicalization tests and identify whether the value lies inside the mechanized domain. Re-signing changes the evidence and is not a substitute for explaining the divergence.

Deployment time

ASSUME-OS-CLOCK · audited_platform · Properties P2, P3, P8

The injected clock is assumed to report operator-accepted Unix time within the deployment tolerance.

If the contract fails. Check the clock actually injected into evaluation against the deployment's accepted tolerance. Reassess time-window and freshness decisions made while that contract failed; changing the tolerance does not establish that previous decisions used valid time.

Atomic local storage

ASSUME-SQLITE-ATOMICITY · audited_storage · Properties P2, P4, P6, P7

SQLite transactions are assumed to provide atomic committed updates for revocation, budget, receipt, and registry state per single-row write. Cross-row crash recovery, ordering, and conservation are not assumed or discharged and remain outside the current formal claim boundary.

If the contract fails. Preserve the affected database and logs, investigate the failed commit boundary and requalify recovery before relying on its state. This assumption covers atomic committed writes; it does not supply cross-row crash recovery or conservation evidence.

Remote endpoint and channel trust

ASSUME-TLS · audited_transport · Properties P8, P9

TLS endpoint authentication and channel confidentiality are assumed for configured remote control and hosted HTTP surfaces.

If the contract fails. Identify the affected endpoint, trust roots and sessions. Restore the required authentication and confidentiality before relying on that channel. Owning the network or adding a second authentication mechanism does not by itself repair a broken TLS contract.

Integrity below message validation

ASSUME-NETWORK-TRANSPORT · audited_transport · Properties P2, P8, P9

Network delivery is not assumed reliable, but authenticated messages received by Chio are assumed not to be silently rewritten below TLS or signature checks.

If the contract fails. Check which bytes reached the authenticated receive boundary and which TLS or signature checks protect that surface. Do not infer that every Chio message has an independent signature, or that authenticated delivery is reliable delivery.

Revocation progress across peers

ASSUME-GOSSIP-FAIRNESS-PARTITION-BOUND · audited_transport · Properties P2

For a configured bilateral revocation peer set, correct connected peers are assumed to have recurring push or catch-up opportunities governed by weak fairness, local clocks remain within the declared skew bound, and declared partitions heal within the operator-declared partition bound. Loss, duplication, reordering, and invalid frames are modeled rather than assumed away. No finite delivery-step or raw-evaluation bound is assumed.

If the contract fails. Compare actual connectivity, recurring catch-up opportunities, clock skew and partition duration with the declared model assumptions. Reassess liveness claims when those conditions fail. The model supplies no finite delivery-step or raw-evaluation-count guarantee.

External registry state

ASSUME-EXTERNAL-REGISTRIES · audited_service · Properties P9, P10

Hosted package, certification, DID, and registry services are assumed to return state they have durably accepted or else fail closed.

If the contract fails. Identify the authority and durable state behind the response. A local mirror introduces its own update and freshness obligations; it does not establish that the upstream service honored its accepted-state contract.

Tool-server process isolation

ASSUME-SUBPROCESS-ISOLATION · audited_platform · Properties P3, P6

Tool-server subprocess isolation and OS process boundaries are assumed for effects outside the pure kernel decision core.

If the contract fails. Treat the affected process boundary as compromised and review the host isolation and reachable resources. A correct kernel authorization decision does not constrain effects that a tool server can perform outside the mediated path.

External settlement finality

ASSUME-CHAIN-FINALITY · audited_external · Properties P4, P7

External chain and oracle finality are assumed only after the configured confirmation/finality policy accepts the evidence.

If the contract fails. Reassess evidence accepted under the affected confirmation or finality policy. More confirmations are a policy change, not a universal repair for a violated chain or oracle assumption.

Runtime trace observation

ASSUME-TRACE-OBSERVER · audited_observability · Properties P2, P4, P10

An installed synchronous runtime trace observer is assumed to receive exactly once before finalization every successful revocation commit, completed tool-call revocation admission, and receipt append. Kernel-assigned source sequences, checked revocation subject identities, exact revocation-source identities, and other callback fields are not rewritten before recording, and the recorder runs without calibration mutations. Delivery reordering is reconciled from source sequences; detectable omissions, duplicates, inconsistent kernel depth limits, ambiguous admission-to-receipt joins, unmatched revocation sources, and relevant revocations between admission and receipt append fail closed. This assumption does not assert that any observed kernel decision is safe.

If the contract fails. Preserve the source sequences, callback accounting, recorder configuration and joins. Detectable omissions and inconsistent joins refuse qualification, but the record still depends on the observer receiving intact callbacks before finalization. A trace cannot independently attest events its trusted observer never received.

Wasm execution boundary

ASSUME-WASM-ENGINE · audited_platform · Properties P3

Wasmtime is assumed to enforce its documented i32 return, trap, fuel-metering, memory-limiter, and in-process sandbox semantics for untrusted guest code.

If the contract fails. Suspend reliance on the affected engine boundary until its required semantics are restored or a replacement is qualified. Advisory mode changes enforcement behavior; it does not repair sandbox isolation or prove the engine's implementation.

Complete finding-status publication

ASSUME-FINDING-STATUS-OPERATOR-COMPLETENESS · audited_service · Properties P4, P7, P10

The qualified cognition-market profile verifies authentic fresh status-feed state but assumes the external status operator inserts every required retraction into that feed.

If the contract fails. Verify the operator's publication process and reconcile required retractions. A fresh authentic feed can still omit an unpublished retraction. Freshness and signatures establish different facts from completeness.

Seller effects beyond observed output

ASSUME-FINDING-SELLER-TOOL-SERVER · audited_service · Properties P3, P6, P10

The qualified cognition-market profile binds kernel-observed seller output bytes and receipts but assumes the seller tool server performs any claimed effect outside Chio's observation boundary.

If the contract fails. If the purchase depends on an external effect, obtain evidence of that effect inside an accepted observation process. The seller's output bytes and their receipt cannot by themselves establish the external event those bytes describe.

Registry consistency

The public assumption registry declares schema chio.formal-assumptions.v1, version 1, and owner formal-verification. The formal proof gate checks the schema, requires the declared required-id set to equal the statement-id set, and compares the approved assumption rows in the claim registry. Owner and version are metadata that the schema check reads as declared.

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

Assumptions in the proof report

The proof report carries assumption identifiers and a count that the checker compares to the registry, and binds the declared property coverage and source artifacts. To assess a result, keep the report's mode, gate statuses, and source identity together with the assumption statement; a matching count shows registry agreement, and the gate statuses show whether proofs ran.

Every release carries a strict report: the gates ran, every one passed, and the report binds to the tag's source commit. Check it, and the assumption count it carries, for the binary you run:

chio release verify --evidence formal

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

Maintainers regenerate and check the report from source as described in Qualification: formal gates. Read how the report is assembled for what each field binds.

Retiring an assumption

The registry lists no retired assumptions, and the proof manifest lists no discharged assumptions. Retiring one takes replacement evidence that the registry names explicitly.

Replacement evidence

Start with the exact contract being replaced. Name the model property and an implementation-refinement gate for the affected production boundary, then show why that evidence supports retiring or narrowing the contract. The registry requires both kinds of evidence; an abstract invariant or a manually recorded mirror hash supplies one at most.

For revocation, the distributed model makes authentication, recurring catch-up opportunities, clock skew, and partition healing explicit. The obligation becomes more precise, and both transport assumptions stay in the register.

Untrusted inputs and trusted enforcement

An agent's requested action, a presented capability, a tool result, or a received peer frame passes the checks for its path into the kernel. An allow verdict authorizes the mediated operation under that configuration; it says nothing about the agent's intent, the truth of a result, or an unobserved external effect.

The enforcement boundary also needs isolation from the host. An in-process Wasm engine, a subprocess sandbox, and a remote service are different dependencies. Switching a guard to advisory mode changes whether its decision blocks execution, and a failed sandbox contract stays failed.

Timing evidence

The dudect harnesses compare timing classes for selected operations. A threshold crossing warrants investigation under the lane's measurement conditions, and a passing run means the experiment stayed under its threshold on that machine. Other machines and other side channels need their own evidence; Constant-Time Tests documents the lane.

Reviewable trust changes

A smaller decision core makes it practical to trace security properties into implementation, as long as the boundary holds: review new inputs, side effects, and dependencies together with the evidence they require. A TEE adds its own hardware, firmware, and attestation trust to the deployment's trusted computing base.

Published claims

Use the public claim registry, proof manifest, theorem inventory, assumption registry, and a qualifying strict report together. The report checker validates structure and source binding. Its gate statuses rely on the trusted generator process, and checking an existing file does not rerun the proofs.