Verified Core Boundary

Chio’s proof boundary is a list of Rust names. A name on it is a claim that some tool reasons about that code; a name off it is a claim about nothing at all. The list lives in one machine-readable file, and the two prose documents that describe it both defer to that file. What follows is which names are on the list, which shell methods may say they reach them, and what being listed does and does not entitle you to say.

The proof methods that work inside the boundary live one section over: Lean 4 Proofs, Kani Harnesses, Creusot Contracts, Aeneas Pipeline, and TLA+ Specs each explain what one tool checks. The Kernel-to-Node split, which is a different line through the same crates, is Core & Shell.

The boundary is one TOML file

Chio’s verified-core contract is machine-readable and lives at formal/proof-manifest.toml. It is not a prose claim with a code appendix; the prose in docs/architecture/CHIO_RUNTIME_BOUNDARIES.md and in spec/PROTOCOL.md section 5.5 both point back at the manifest and say the manifest is the definition. The manifest names its own status, its own anchors, and its own registries in its first eleven lines.

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

Read implementation_linked_protocol_core literally. The manifest’s own note spells out what it means: the covered region is the pure security decision logic plus, in its words, "bounded models for adjacent state transitions", and "concrete platform effects are tracked as audited assumptions". Two claims are being made at once. The decision logic is linked to shipped Rust. The transitions around it are linked to bounded models that stand in for shipped Rust, and the models are not the Rust.

The file is larger than the boundary it draws. It carries 37 Lean root modules, a property_matrix of 10 entries covering P1 through P10, 5 refinement lanes, a list of named exclusions, a set of gate commands, and a run of [[mirror]] blocks pinning per-symbol SHA-256 hashes between Rust sources and Lean or TLA+ models. Exactly one axiom is allowed anywhere in the Lean development, Chio.Json.hash_collision_resistant, and formal/theorem-inventory.json registers it one to one as ASSUME-SHA256, with concrete SHA-256 left outside Lean. The parts a Kernel reader needs are the two lists below.

The covered pure core

The boundary document and the protocol spec agree on the same four entries, naming six functions between them, and both present those as the pure Rust the current claim rests on. Every one lives in chio-kernel-core, the crate that declares #![no_std] and #![deny(unsafe_code)] in its lib.rs.

The manifest itself is broader than that table. Its covered_rust_symbols array holds 47 entries and its covered_rust_modules array holds 13 module paths. The two lists do not line up. The symbols sit in 17 distinct modules, 4 of which the manifest never declares: 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 only under the revocation-view feature, which is on by default for hosted builds and off for the portable no_std one, so the covered symbol RevocationView::install_if_newer is absent from the very build the boundary is drawn around.

Fewer of them sit in chio-kernel-core than a reader of the boundary document would guess: 33 of the 47. 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.

The six named in the table above are the ones the spec elevates as the pure decision core; the remaining 41 are supporting predicates and bounded models, and the difference between the two groups is the whole subject of the theorem inventory.

The predicate module underneath

One file holds 18 of the covered symbols, crates/kernel/chio-kernel-core/src/formal_core.rs, whose module header states the constraint that earns it the listing: 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 takes four bools. receipt_fields_coupled takes five. composite_quota_authorize takes three fixed-size arrays and returns a CompositeQuotaResult that returns the input unchanged on any refusal.

That shape is what makes them provable and what limits what a proof about them says. A theorem about guard_pipeline_allows(core_authorized, guards) establishes that deny and error are both absorbing over a slice of GuardStep values. It establishes nothing about whether the runtime built the right slice.

Two shell entry points, and what "direct" means

The pure core is a library. Something in chio-kernel has to call it, and the moment it does, the caller is running with a tokio runtime, a SQLite handle, and mutable state. The boundary document handles that by naming exactly two methods that may claim to reach the pure core directly. The spec puts it as "the two shell entrypoints that may claim direct use of that pure core today".

Both methods carry the claim in their own doc comments, which is the part that makes the boundary auditable from the code rather than only from the manifest. evaluate_portable_verdict is annotated as "the one chio-kernel entrypoint inside the current bounded verified core". build_and_sign_receipt is annotated as included "only for the direct call" into core signing, with body assembly, metadata shaping, and persistence named as shell behavior outside the claim.

The manifest carries a wider list than the pair. Its shell_entrypoints array also names 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. Those are the shell surfaces a model projects. The two in the table are the only ones the boundary document lets a shell method claim as a direct call into the pure core.

Read the actual call, though, because neither method calls the symbol the manifest lists. evaluate_portable_verdict does three fail-closed checks of its own and then calls a wider entry point in the same core module.

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,
    )
}

evaluate_with_full_floor_and_root verifies through verify_capability_full_with_root, rejects aggregate_invocation_budget and cumulative approval as unsupported features, and then hands off to finish_verified_evaluation, which is where subject binding, scope match, and the guard pipeline actually run. evaluate reaches the same private tail through a narrower door. So the shared covered region is the tail, not the entry; the manifest lists both evaluate and finish_verified_evaluation for that reason, and the three fail-closed checks evaluate_portable_verdict runs before the call, plus the trust-root snapshot it takes between them, are shell behavior on both sides of the boundary.

The signing path is cleaner, because the wider function is a thin forwarder. build_and_sign_receipt calls chio_kernel_core::sign_receipt_with_handle, which consumes a one-time ReceiptSigningHandle by value and forwards its canonical bytes straight into sign_receipt, the listed symbol. The crate marks one thing about that handle as unfinished. Producers still build it from canonical content they supply rather than receiving it from evaluate, and the seam note on sign_receipt_with_handle names the intended end state: have evaluate() return the handle so the only way to obtain one is to have run an evaluation. On the kernel path the preimage is the exact bytes receipt_content_for_output hashed, which is what makes the gate non-tautological there.

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 (receipt_persistence.rs:176-190).

build_and_sign_receipt is pub(crate) and forwards in one line to build_and_sign_receipt_with_authority, which is where the coupling check, the handle, and the boundary note above actually sit. The manifest lists the outer name.

The audited assumptions

Everything the pure core touches but does not implement is registered in formal/assumptions.toml under schema chio.formal-assumptions.v1. Each entry is one pipe-delimited line carrying an id, a classification, a contract sentence, and the property ids it supports. There are 15 of them, in 8 classes. The registry is enforced: scripts/check-formal-proofs.sh fails when the set of ids in required_assumption_ids differs from the set actually defined, in either direction, and it refuses any entry whose line does not carry all four fields.

Two entries in that table are worth reading twice. ASSUME-SHA256 is the one the Lean development is allowed to axiomatize, and ASSUME-TRACE-OBSERVER closes with the line that bounds the whole registry: it "does not assert that any observed kernel decision is safe".

None of them has been retired. retired_assumption_ids and retired_assumptions are both empty arrays, and so is the manifest’s discharged_assumptions. The registry states the bar for changing that: 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".

One near-miss is recorded in full, and it is the honest kind. The distributed-revocation model in formal/tla/DistributedRevocation.tla supplies the distributed-time story the transport assumption was standing in for, and its StaleEvaluationDenied invariant mirrors the production wall-clock freshness gate. That could plausibly have retired the broad transport assumption. It did not, and the manifest carries the decision as a field: m04_p5_t5_assumptions_decision = "ASSUME-NETWORK-TRANSPORT-scoped-not-retired", beside a m04_p5_t5_rationale_anchor pointing at formal/tla/DistributedRevocation.tla::StaleEvaluationDenied. The reason is in the comment above the field, and it is about what the model does not reach: the broad transport assumption "remains required alongside the narrower named fairness and partition assumption", and "weak fairness does not prove a finite evaluation-count bound". The model’s own header says the same thing from the other end, naming RejectedRawEvaluationCountBound as deliberately outside SafetyInv with a registered witness that arbitrary loss permits more evaluations than any finite count. What stands in for that is operational, not formal: the signer-id pin and signature check in crates/trust/chio-federation/src/revocation_gossip.rs run before RevocationView::install_if_newer, and the registry closes on the same note, that the distributed model "scopes authentication, weak fairness, skew, and partition-heal obligations, but does not retire either transport assumption". Scoping an assumption is not discharging it. Assumptions & TCB works through each entry.

What is named as outside

The manifest also lists its exclusions by name in excluded_surfaces, which is a different register from the assumptions: an assumption is something Chio relies on and audits, an exclusion is something Chio makes no claim about at all. The boundary document condenses them to four bullets. The machine-readable list is finer, and three entries are worth reading closely.

• Reservation-ledger refinement from the pure ledger_apply model to concrete BudgetStore mutations. Runtime debug replay and stateful tests are listed as evidence and explicitly not as a proof of refinement.
• Cross-row receipt and budget crash recovery, ordering, and conservation, held out until implementation trace validation and crash-reopen gates establish refinement. That is the same line ASSUME-SQLITE-ATOMICITY draws from the other side.
• Float-valued JSON leaves in action, metadata, or other compound receipt-id fields. Their production rendering is covered by frozen vectors and ASSUME-CANONICAL-JSON, not by the mechanized canonical-JSON domain.

The remaining nine cover concrete 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.

What holds the boundary in place

Three of the manifest’s gate_commands entries are what keep the claims above from drifting, and each checks something narrower than its name suggests. A fourth check, the boundary document’s own regression test, is not a manifest gate at all; it is a cargo test in a platform crate, and it belongs here because it is the only automated thing standing between the boundary document and silent edits.

Underneath those, the Kani lane is the one that touches these exact symbols. formal/rust-verification/kani-public-harnesses.toml puts every harness it registers in lanes.pr, leaves lanes.nightly_only an empty array, and drives them from scripts/check-kani-public-core.sh. The comment above the lane assignment gives the reason and the cost: the full sweep is "~2.2 min locally, within the 10-minute warm PR target". Both Kani registries and the Creusot registry are marked required in rust_refinement_lanes; both Aeneas lanes are marked pilot and production. The manifest summarizes the division: Creusot and Kani are "required strict-CI lanes for production implementation linkage", and the public Kani harnesses "target verify_capability, NormalizedScope::is_subset_of, resolve_matching_grants, evaluate, sign_receipt, and the shared budget and revocation admission projections". That is a nearby split, not an identical one. The Kani list adds NormalizedScope::is_subset_of, which the boundary document’s four entries do not name, and drops the two companion functions verify_capability_with_trusted and resolve_capability_grants. Its own covered_symbols array is wider than either, reaching PublicKey::verify_canonical in chio-core-types and compute_slash_allocation in chio-open-market.

Guarantees and limits

Next steps

• Formal Assurance Overview · the same boundary from the proof side, with the reading paths by role
• Assumptions & TCB · each registry entry worked through, and what retiring one would take
• Kani Harnesses · the lane that touches these exact symbols, its bounds, and what a bounded proof settles
• Core & Shell · the other line through the same crates: what pure evaluation excludes, and why
• Portable Kernel Core · the four build shapes the covered crate compiles into, and the two platform inputs it takes