Verified Core Boundary

One TOML file draws the boundary

The manifest is the definition. docs/architecture/CHIO_RUNTIME_BOUNDARIES.md and spec/PROTOCOL.md section 5.5 both defer to it, and the manifest names them back as boundary_doc and spec_anchor.

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

Its status, implementation_linked_protocol_core, makes two claims at once. In the manifest’s own note, the covered region is the pure security decision logic plus “bounded models for adjacent state transitions”, and “concrete platform effects are tracked as audited assumptions”. The decision logic is linked to shipped Rust; the transitions around it are linked to bounded models that stand in for that Rust.

The file holds more than the boundary: 37 Lean root modules, a property_matrix of 10 entries covering P1 through P10 (P10, report truthfulness, is a claim about reports), 5 refinement lanes, named exclusions, gate commands, and [[mirror]] blocks pinning per-symbol SHA-256 hashes between Rust sources and Lean or TLA+ models. Exactly one axiom is allowed in the Lean development, Chio.Json.hash_collision_resistant, which formal/theorem-inventory.json registers one to one as ASSUME-SHA256, leaving the SHA-256 implementation outside Lean.

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"]
pilot_toolchain = ["aeneas"]

To apply a claim, find the entry point your integration calls, its Rust subject and proof method in the manifest, and the assumptions and exclusions that bound it. A registry entry names the subject; the method’s evidence supplies the checked scope.

Six pure functions form the covered decision core

The boundary document and the protocol spec list the same four entries. All six functions live in chio-kernel-core, the crate that declares #![no_std] and #![deny(unsafe_code)].

• capability_verify::verify_capability, verify_capability_with_trusted. Decide signature, issuer trust, and time bounds over one in-memory token, returning VerifiedCapability or a CapabilityError. Their doc comment leaves delegation-chain validation, revocation lookup, and subject binding to the caller. They fix the crypto floor at CapabilityCryptoFloor::AllowClassical and run a NoopBudgetRegistry; a kernel that loads policy.crypto_floor calls verify_capability_with_floor.
• scope::resolve_matching_grants, resolve_capability_grants. Decide which grants cover a (server, tool, Invoke) request, sorted by a (server-exact, tool-exact, constraint-count) specificity tuple. A constraint that needs regex or IO returns ScopeMatchError::ConstraintError.
• evaluate::evaluate. Runs capability verification, subject binding on agent_id, the portable scope match, then the guard pipeline, fail-closed at each step. Budget mutation, revocation lookup, dispatch, and persistence belong to the caller. As the AllowClassical wrapper, it denies when attenuation_proof is present, because chain binding needs a trust-root resolver.
• receipts::sign_receipt. Recomputes sha256_hex(canonical_content) inside the trust boundary, refuses on disagreement with body.content_hash, then checks the kernel key and signs. The receipt body arrives fully formed.

The manifest’s covered_rust_symbols array is wider: 47 entries in 17 modules, while covered_rust_modules declares 13 module paths. The modules holding symbols outside that declared list are chio_core_types::capability, chio_core_types::delegation_receipt, chio_kernel_core::revocation_view, and chio_revocation_oracle::api. chio_kernel_core::revocation_view compiles under the revocation-view feature, on for hosted builds and off for the portable no_std one, so the covered RevocationView::install_if_newer belongs to the hosted build.

33 of the 47 symbols sit in chio-kernel-core. The rest reach into chio-core-types Merkle walks and capability delegation, chio-federation revocation gossip, chio-credit scalar conversion, chio-web3 settlement state ids, chio-open-market slash allocation, and the chio-revocation-oracle inclusion proof; by crate, chio_federation 5, chio_core_types 4, chio_credit 2, chio_open_market 1, chio_revocation_oracle 1, chio_web3 1. The six named above are the decision core; the other 41 are supporting predicates and bounded models, listed in the theorem inventory.

crates/kernel/chio-kernel-core/src/formal_core.rs holds 18 of the covered symbols. Its module header states the constraint: it “deliberately avoids heap allocation, IO, crypto, async, and external crates so Kani, Creusot wrappers, and Aeneas can reason about the same branch logic used by the portable kernel core”. Every function in it is total over scalars, booleans, small enums, and fixed-size arrays: budget_precheck takes four u64s, dpop_admits four bools, receipt_fields_coupled five, and composite_quota_authorize three fixed-size arrays, returning a CompositeQuotaResult that carries the input unchanged on any refusal. A theorem about guard_pipeline_allows(core_authorized, guards) establishes that deny and error are absorbing over a slice of GuardStep values; whether the runtime built the right slice is a separate question.

Two shell methods reach the core through wider calls

Any chio-kernel caller of the pure core runs with a tokio runtime, a SQLite handle, and mutable state. The boundary document and the spec name the two shell methods that may claim to reach the core directly.

Both carry the claim in their doc comments, so the boundary is auditable from the code. evaluate_portable_verdict is “the one chio-kernel entrypoint inside the current bounded verified core”, supplying trusted issuers and portable guard wiring. build_and_sign_receipt is included “only for the direct call” into core signing, after the shell assembles the body; body assembly, metadata shaping, and persistence are shell behavior. The manifest’s shell_entrypoints array also lists ChioKernel::check_revocation, ChioKernel::run_guards, DpopNonceStore::check_and_insert_through, both budget-store charge paths in chio-kernel and chio-store-sqlite, and receipt_body_fields_coupled: the shell surfaces a model projects.

evaluate_portable_verdict runs three fail-closed checks of its own (capability negotiation, the negotiated capability root, and the budget-registry lock, where a poisoned lock denies and calls record_tcb_lock_poison) and takes a trust-root resolver snapshot, which has no failure arm. It then calls evaluate_with_full_floor_and_root, which verifies through verify_capability_full_with_root, rejects aggregate_invocation_budget and cumulative approval as unsupported features, and hands off to finish_verified_evaluation, where subject binding, scope match, and the guard pipeline run. evaluate reaches the same private tail through a narrower door, so the manifest lists both, and the checks before the call are shell behavior.

pub fn evaluate_portable_verdict<'a>(
    &self,
    capability: &'a CapabilityToken,
    request: &chio_kernel_core::PortableToolCallRequest,
    guards: &'a [&'a dyn chio_kernel_core::Guard],
    clock: &'a dyn chio_kernel_core::Clock,
    session_filesystem_roots: Option<&'a [String]>,
) -> chio_kernel_core::EvaluationVerdict {
    let trusted = self.trusted_issuer_keys();
    let peer_profile = match self.capability_negotiation_for_remote(None, clock.now_unix_secs())
    {
        Ok(profile) => profile,
        // Fail closed: a negotiation error denies rather than falling back
        // to the permissive default profile.
        Err(reason) => {
            return chio_kernel_core::EvaluationVerdict {
                verdict: chio_kernel_core::Verdict::Deny,
                reason: Some(format!(
                    "capability negotiation failed; denying fail-closed: {reason}"
                )),
                matched_grant_index: None,
                verified: None,
            };
        }
    };
    let trust_resolver = self.capability_trust_root_resolver_snapshot();
    let direct_root = match self.negotiated_capability_root(capability, &peer_profile) {
        Ok(root) => root,
        Err(reason) => {
            return chio_kernel_core::EvaluationVerdict {
                verdict: chio_kernel_core::Verdict::Deny,
                reason: Some(reason),
                matched_grant_index: None,
                verified: None,
            };
        }
    };
    let mut budgets = match self.budget_registry.lock() {
        Ok(guard) => guard,
        Err(_poisoned) => {
            // The monetary lock is poisoned: a panic left the registry in an
            // unknown state. Deny fail-closed and trip the degraded flag so
            // later evaluations are denied at the pre-dispatch gate too.
            self.record_tcb_lock_poison("budget_registry");
            return chio_kernel_core::EvaluationVerdict {
                verdict: chio_kernel_core::Verdict::Deny,
                reason: Some("budget registry lock poisoned; denying fail-closed".to_string()),
                matched_grant_index: None,
                verified: None,
            };
        }
    };
    chio_kernel_core::evaluate_with_full_floor_and_root(
        chio_kernel_core::EvaluateInput {
            request,
            capability,
            trusted_issuers: &trusted,
            clock,
            guards,
            session_filesystem_roots,
        },
        capability_crypto_floor(self.capability_crypto_floor),
        &peer_profile,
        direct_root.as_ref(),
        &trust_resolver,
        &mut *budgets,
    )
}

build_and_sign_receipt forwards in one line to build_and_sign_receipt_with_authority, which holds the coupling check, the handle, and the boundary note, and calls chio_kernel_core::sign_receipt_with_handle. That function consumes a one-time ReceiptSigningHandle by value and passes its canonical bytes to sign_receipt, the listed symbol. On the kernel path the preimage is the exact bytes receipt_content_for_output hashed, which keeps the recompute gate meaningful.

require_receipt_body_fields_coupled(&body, &expected)?;

// WYSIWYS: bind the signature to the exact content this receipt's
// `content_hash` was derived from. The handle recomputes
// `sha256_hex(canonical_content)` and the signing primitive refuses to
// sign if it disagrees with `body.content_hash`, closing the
// render-A / sign-B hole on the production path. The
// canonical_content is the same preimage `receipt_content_for_output`
// hashed to produce `content_hash`.
let handle = ReceiptSigningHandle::from_content_preimage(params.canonical_content);

// ...

// Verified-core boundary note:
// `formal/proof-manifest.toml` includes this shell method only for the
// direct call into `chio_kernel_core::sign_receipt_with_handle`. Receipt
// body assembly, metadata shaping, and persistence remain
// operational-shell behavior outside the current bounded proof claim.
let backend = chio_core::crypto::Ed25519Backend::new(authority.clone());
chio_kernel_core::sign_receipt_with_handle(body, &backend, handle).map_err(|error| {
    // ...
})

The elided closure maps KernelKeyMismatch, ContentHashMismatch, and SigningFailed onto KernelError::ReceiptSigningFailed. One signer skips the recompute: sign_receipt_relaying_trusted_body serves the thin FFI and WASM transport adapters that receive an already-minted body without its preimage, and it still enforces the kernel-key match. The spec requires every path that holds the evaluated content to call sign_receipt or sign_receipt_with_handle. The relay function sits outside covered_rust_symbols as a reviewed convention, named as its own function so that trust is auditable in one place; Receipt Contract covers the signing contract in full.

Audited assumptions and named exclusions carry the rest

formal/assumptions.toml, schema chio.formal-assumptions.v1, registers everything the core touches without implementing: Ed25519, SHA-256, canonical JSON, TLS, the OS clock, SQLite, chain finality, wasmtime, subprocess isolation, hosted registries, network transport, gossip fairness, the trace observer, and two cognition-market operator boundaries. Each entry is one pipe-delimited line carrying an id, a classification, a contract sentence, and the property ids it supports. The formal proof gate fails when required_assumption_ids differs from the defined set in either direction, and refuses any line missing one of the four fields.

ASSUME-SHA256 is the one the Lean development may axiomatize. ASSUME-TRACE-OBSERVER closes with the line that bounds the registry: it “does not assert that any observed kernel decision is safe”. retired_assumption_ids, retired_assumptions, and the manifest’s discharged_assumptions are all empty. Retiring an assumption “requires named model evidence and a concrete implementation-refinement gate over the affected production boundary”, and “abstract invariants and manual mirror hashes are not sufficient by themselves”. Assumptions & TCB lists every entry with its contract.

formal/tla/DistributedRevocation.tla scopes the transport assumption without retiring it. Its StaleEvaluationDenied invariant mirrors the production wall-clock freshness gate, and the manifest records ASSUME-NETWORK-TRANSPORT-scoped-not-retired against it, because “weak fairness does not prove a finite evaluation-count bound”; the broad assumption stays beside the narrower ASSUME-GOSSIP-FAIRNESS-PARTITION-BOUND, and the model scopes authentication, weak fairness, skew, and partition-heal obligations. The model keeps RejectedRawEvaluationCountBound outside SafetyInv, with a registered witness that arbitrary loss permits more evaluations than any finite count. The signer-id pin and signature check in crates/trust/chio-federation/src/revocation_gossip.rs run before RevocationView::install_if_newer and cover that ground operationally.

• Reservation-ledger refinement. From the pure ledger_apply model to the runtime BudgetStore mutations. Runtime debug replay and stateful tests are listed as evidence, and as evidence only.
• Cross-row crash recovery. Receipt and budget crash recovery, ordering, and conservation, held out until implementation trace validation and crash-reopen gates establish refinement; ASSUME-SQLITE-ATOMICITY draws the same line from the other side.
• Float-valued JSON leaves. In action, metadata, or other compound receipt-id fields, covered by frozen vectors and ASSUME-CANONICAL-JSON outside the mechanized canonical-JSON domain.

Nine more excluded_surfaces entries cover cryptography and platform implementations, effects after the decision core allows a call, cluster consensus and settlement rails, Aeneas extraction from async and IO-heavy modules, symlink resolution and OS filesystem root enforcement, treaty predicate parsing and hashing outside its decision domain, the canonical-JSON refinement to chio-core-types/src/canonical.rs beyond checked fixtures, the trace-observer callback boundary, and wasmtime engine behavior beyond typed verdict dispatch. The boundary document condenses these into four bullets. An assumption is something Chio relies on and audits; an exclusion is outside the claim entirely.

Three gates and one test keep the boundary from drifting

Three gate_commands entries and one cargo test hold the claims above in place:

1. The formal proof gate. The manifest schema is chio.proof-manifest.v1; every root_modules and covered_rust_modules path exists; the assumption registry parses and its declared and defined id sets are equal; every refinement lane is well-formed. It reads Lean structure down to per-file namespace, open, export, and abbrev controls and the declared theorem set. For Rust modules it checks the path.
2. The proof-coverage check. Every covered symbol resolves to a workspace crate and, where possible, a module file: surface_from_symbol splits on ::, resolves the crate, and tries src/<module>.rs, then src/<module>/mod.rs.
3. The formal-mirrors check. Per-symbol and rollup SHA-256 over normalized token streams in the [[mirror]] blocks, so any edit to a mirrored Rust symbol forces a model review. Matching hashes, in the manifest’s words, “do not prove semantic equivalence or modeled properties”.
4. crates/platform/chio-control-plane/tests/runtime_boundaries.rs. runtime_boundary_map_is_present asserts that the boundary document exists and names eight ownership paths, plus line-count ceilings on four runtime shells.

All four run before every release is tagged, beside the public Kani lane, and the release's signed proof report records their results against the tag's source commit. Check them 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 run the gates from source as Qualification: formal gates describes.

The Kani lane touches these exact symbols. formal/rust-verification/kani-public-harnesses.toml puts every harness in lanes.pr, leaves lanes.nightly_only empty, and drives them from the public Kani runner; public_sign_receipt_refuses_content_hash_mismatch and public_sign_receipt_accepts_matching_content_hash cover both arms of the recompute gate. Both Kani registries and the Creusot registry are required in rust_refinement_lanes, and the public harnesses “target verify_capability, NormalizedScope::is_subset_of, resolve_matching_grants, evaluate, sign_receipt, and the shared budget and revocation admission projections”. That list adds NormalizedScope::is_subset_of and drops verify_capability_with_trusted and resolve_capability_grants; its covered_symbols array reaches further, to PublicKey::verify_canonical in chio-core-types and compute_slash_allocation in chio-open-market.

Under --cfg kani, symbolic execution cannot run RFC 8785 canonicalization or curve arithmetic in budget, so three functions take a different branch. In receipts.rs, sign_receipt_relaying_trusted_body, the tail sign_receipt forwards into, returns a ChioReceipt signed over b"kani-receipt-signing-model", with the production ChioReceipt::sign_with_backend call behind #[cfg(not(kani))]. In scope.rs, resolve_matching_grants takes a single-grant fast path and the private matches_pattern a byte-level prelude. Of the three, only resolve_matching_grants is itself in covered_rust_symbols; the other two sit in covered modules. The harnesses are proofs about the branch they execute: the recompute-and-refuse gate and the kernel-key check are on the shared path, and the canonical-JSON encode and Ed25519 signature beneath them rest on ASSUME-CANONICAL-JSON and ASSUME-ED25519.

Next: the proofs inside the boundary