Formal assurance

Selected Rust decisions are extracted into Lean and tied to their models by theorems, each claim with its boundary stated.

On this page

Agent applications depend on authority rules that hold as they add workers, delegate work, and share resources. Formal verification can establish specific properties of those rules. Each claim needs a named property, the code that relies on it, and the assumptions under which the proof holds.

Chio extracts selected production Rust functions into Lean and connects them to protocol models through equivalence theorems. The runtime calls these functions where it acts on their results. The evidence reaches concrete decisions about authority, budgets, replay admission, guards, and receipt construction.

The proof manifest and the claim registry fix the boundaries: a named property, the methods that check it, the code that uses it, and the assumptions it inherits.

Trace one proof to a signing gate

Before the kernel signs a mediated-decision receipt, it checks that the receipt’s fields agree with the request and decision it attests. A correctly signed record with the wrong request, authority, or evidence class would still be the wrong record, so the check sits on the signing path rather than in a later audit.

The check reduces to one Boolean function over five comparisons, and that function is the part the formal evidence covers:

\mathrm{coupled}(c, r, v, p, e) \;=\; c \wedge r \wedge v \wedge p \wedge e

Here $c$ says the capability matches, $r$ the request, $v$ the verdict, $p$ the policy hash, and $e$ the evidence class. Five artifacts connect that function to the running kernel and to its model:

Step	Where it lives	What it settles
Project the fields	`receipt_body_fields_coupled` in `receipt_support/coupling.rs`	Compares the assembled receipt with its expected capability, request, decision, policy hash, and evidence classification, producing the five Booleans.
Require all five	`receipt_fields_coupled` in `chio-kernel-core`	Returns their conjunction. A Creusot contract states the same equation over the Rust source.
Gate the signature	`require_receipt_body_fields_coupled` in `receipt_persistence.rs`	Refuses to sign with `ReceiptSigningFailed` when the check fails, before the signing primitive runs.
Extract	The `decision_core` target in `formal/aeneas/production.toml`	Aeneas translates the Rust helper into a generated Lean definition.
Prove equal	`generated_receipt_fields_coupled_eq_mirror`	For every combination of the five inputs, the generated definition equals the mirror model of receipt-field coupling.

The helper is small enough to read whole. Its contract and its body state the same conjunction:

chio-kernel-core/src/formal_aeneas.rs354–376rust

#[cfg_attr(
    chio_creusot_contracts,
    ensures(result == (
        capability_matches
            && request_matches
            && verdict_matches
            && policy_hash_matches
            && evidence_class_matches
    ))
)]
pub fn receipt_fields_coupled(
    capability_matches: bool,
    request_matches: bool,
    verdict_matches: bool,
    policy_hash_matches: bool,
    evidence_class_matches: bool,
) -> bool {
    capability_matches
        && request_matches
        && verdict_matches
        && policy_hash_matches
        && evidence_class_matches
}

The equivalence theorem closes the link from the extracted definition to the model. Its proof splits on the Boolean inputs, so it holds for every case rather than for sampled ones:

formal/lean4/Chio/Chio/Proofs/AeneasGeneratedEquivalence.lean769–782lean

theorem generated_receipt_fields_coupled_eq_mirror
    (capabilityMatches requestMatches verdictMatches policyHashMatches
      evidenceClassMatches : Bool) :
    Chio.AeneasProduction.receipt_fields_coupled
        capabilityMatches requestMatches verdictMatches policyHashMatches evidenceClassMatches =
      ok (AeneasMirror.receiptFieldsCoupled {
        capabilityMatches,
        requestMatches,
        verdictMatches,
        policyHashMatches,
        evidenceClassMatches,
      }) := by
  cases capabilityMatches <;> cases requestMatches <;> cases verdictMatches <;>
    cases policyHashMatches <;> rfl

Production code calls the helper covered by the registered theorem. That theorem proves the conjunction. The field projections that produce its inputs, and the concrete signature that follows, are adjacent pieces with their own evidence: tests, review, and the cryptographic assumptions below.

Read the field projection and the signing gate

chio-kernel/src/receipt_support/coupling.rs19–48rust

/// Compare an assembled receipt body with the decision inputs it must attest.
#[must_use]
pub fn receipt_body_fields_coupled(
    body: &ChioReceiptBody,
    expected: &ReceiptCouplingExpectation<'_>,
) -> bool {
    let capability_matches = body.capability_id == expected.capability_id;
    let request_matches = body.tool_server == expected.server_id
        && body.tool_name == expected.tool_name
        && body.action.parameters == expected.action.parameters
        && body.action.parameter_hash == expected.action.parameter_hash
        && body.content_hash == expected.content_hash;
    let verdict_matches = body.decision.as_ref() == Some(expected.decision);
    let policy_hash_matches = body.policy_hash == expected.policy_hash;
    let evidence_class_matches = body.receipt_kind == ReceiptKind::MediatedDecision
        && body.boundary_class == BoundaryClass::Prevent
        && body.observation_outcome.is_none()
        && body.tool_origin == ToolOrigin::CallerExecuted
        && body.redaction_mode == RedactionMode::None
        && body.actor_chain.is_empty()
        && body.trust_level == expected.trust_level;

    chio_kernel_core::receipt_fields_coupled(
        capability_matches,
        request_matches,
        verdict_matches,
        policy_hash_matches,
        evidence_class_matches,
    )
}

chio-kernel/src/kernel/responses/receipt_persistence.rs3–14rust

fn require_receipt_body_fields_coupled(
    body: &ChioReceiptBody,
    expected: &ReceiptCouplingExpectation<'_>,
) -> Result<(), KernelError> {
    if receipt_body_fields_coupled(body, expected) {
        Ok(())
    } else {
        Err(KernelError::ReceiptSigningFailed(
            "receipt fields diverged from the admitted decision inputs".to_string(),
        ))
    }
}

Receipt coupling projects rich receipt fields into comparisons.
The core helper surface delegates the decision to extraction-safe Rust.
The production extraction manifest identifies the source and generated artifacts.
Generated equivalence theorems connect the extracted definition to the model.
Receipt persistence requires the check before signing.

Ten properties, each with its own evidence

Receipt coupling is one link in a larger register. The claim registry organizes the protocol properties as P1 through P10 and specifies the strength of language each supports. The proof manifest records, for each property, the lanes that check it, the assumptions it depends on, its implementation links, and its exclusions.

P4, receipt integrity: 7 registered lanes and 13 named entries.

\begin{aligned} \htmlClass{role-seal}{m_p} &= \textstyle\sum_\ell \htmlClass{cor-relation}{M_{\ell p}} \quad \text{lanes per property} \\ \htmlClass{role-seal}{n_\ell} &= \textstyle\sum_p \htmlClass{cor-relation}{M_{\ell p}} \quad \text{properties per lane} \end{aligned}

In the proof manifest · proof-manifest.toml:160

property_matrix = [
  # …
  "P4|receipt integrity|lean_root_imported,symbolic_crypto,audited_crypto_assumption,receipt_totality,aeneas_equivalence,public_kani,differential_test|proof.canonical_inj,proof.receipt_id_input_collision_resistant,proof.receipt_id_collision_resistant,proof.membership_proof_sound,proof.stepFold_eq_applyProof,proof.stepFold_membership_sound_if_geometry_agrees,proof.boundedWalkGeometry_decodes,proof.bounded_stepFold_sound,proof.generated_inclusion_step_eq_model,proof.receipt_sign_then_verify,proof.receipt_immutability,proof.receiptFieldsCoupled_preserves_all_fields,proof.generated_receipt_fields_coupled_eq_model",
  # …
]

Rows are the lanes the proof manifest registers for properties P1 to P10; hatched rows are audited assumptions rather than methods. Counts describe registration, not a share of the runtime proved, and a registered lane is not evidence that a given revision passed it.

The matrix groups evidence by property and by verification method or assumption. P1 concerns attenuation: delegated authority must preserve or narrow the parent’s permission. P10 concerns evidence classification: modeled report and export labels cannot promote asserted or observed evidence to verified evidence. These are specific protocol properties, not claims that an arbitrary agent report is true. The matrix shows what is registered; for a claim under review, use the check’s result at that source revision.

Different methods examine different boundaries

Each verification method checks a defined statement about a particular model or implementation:

Method	Evidence it provides
Lean 4	Machine-checked theorems over the registered definitions and assumptions, including bounded protocol models and extracted-code equivalence.
Aeneas and Charon	A translation from selected Rust functions to Lean definitions, which equivalence theorems connect to the model.
Creusot	Function-contract obligations over selected Rust source: preconditions, postconditions, and invariants.
Kani	Bounded exploration of Rust harnesses for assertions, panics, and other specified properties.
TLA+ and Apalache	Checks of registered state-machine properties within the model and its declared bounds.
Differential tests	Comparisons between implementation and reference behavior for the generated or selected inputs exercised.

The production extraction manifest spans decision-core helpers, reservation-ledger transitions, a scalar Merkle-walk step, and economy conversion helpers. Each target carries its own qualification boundary. The decision-core target alone extracts fifteen functions, from time-window and scope-coverage checks to budget commits, guard steps, revocation snapshots, and receipt coupling:

Read the decision-core extraction target

formal/aeneas/production.tomltoml

name = "decision_core"
source = "kernel_core"
status = "generated_equivalence"
types = [
  "BudgetCommitResult",
]
functions = [
  "classify_time_window_code",
  "time_window_valid",
  "exact_or_wildcard_covers_by_flags",
  "prefix_wildcard_or_exact_covers_by_flags",
  "optional_u32_cap_is_subset",
  "required_true_is_preserved",
  "monetary_cap_is_subset_by_parts",
  "budget_precheck",
  "budget_commit",
  "dpop_freshness_valid",
  "dpop_admits",
  "nonce_admits",
  "guard_step_allows",
  "revocation_snapshot_denies",
  "receipt_fields_coupled",
]
equivalence_theorems = [
  "classify_time_window_code|Chio.Proofs.generated_classify_time_window_code_eq_mirror",
  "time_window_valid|Chio.Proofs.generated_time_window_valid_eq_mirror",
  "exact_or_wildcard_covers_by_flags|Chio.Proofs.generated_exact_or_wildcard_covers_by_flags_eq_mirror",
  "prefix_wildcard_or_exact_covers_by_flags|Chio.Proofs.generated_prefix_wildcard_or_exact_covers_by_flags_eq_mirror",
  "optional_u32_cap_is_subset|Chio.Proofs.generated_optional_u32_cap_is_subset_eq_mirror",
  "required_true_is_preserved|Chio.Proofs.generated_required_true_is_preserved_eq_mirror",
  "monetary_cap_is_subset_by_parts|Chio.Proofs.generated_monetary_cap_is_subset_by_parts_eq_mirror",
  "budget_precheck|Chio.Proofs.generated_budget_precheck_eq_mirror",
  "budget_commit|Chio.Proofs.generated_budget_commit_eq_mirror",
  "dpop_freshness_valid|Chio.Proofs.generated_dpop_freshness_valid_eq_mirror",
  "dpop_admits|Chio.Proofs.generated_dpop_admits_eq_mirror",
  "nonce_admits|Chio.Proofs.generated_nonce_admits_eq_mirror",
  "guard_step_allows|Chio.Proofs.generated_guard_step_allows_eq_mirror",
  "revocation_snapshot_denies|Chio.Proofs.generated_revocation_snapshot_denies_eq_mirror",
  "receipt_fields_coupled|Chio.Proofs.generated_receipt_fields_coupled_eq_mirror",

Inspect the generated theorem catalog

The documentation snapshot contains 165 theorem entries. The categories below describe the catalog, not a percentage of the runtime that has been proved.

Claim class	Entries
`aeneas_equivalence`	32
`bounded_model`	122
`symbolic_crypto`	11

Read the theorem inventory for the named statements and sources.

Every proof has an edge

A theorem about a pure helper establishes its stated property over the modeled inputs. Runtime callers still have to derive those inputs correctly, act on the result, and preserve the required state. The receipt example shows the pattern: the conjunction is proved, and the comparisons that feed it are a separate, adjacent piece of evidence.

Included subject	Boundary to retain
Extracted reservation-ledger decisions	Agreement with bounded transition models does not establish refinement to every concrete budget-store mutation.
Scalar economy conversion	Rounding properties do not establish collection conservation or production netting behavior.
Merkle inclusion walk	Registered refinement reaches the stated bound of eight leaves and retains the SHA-256 assumption.
Symbolic receipt and signature models	Concrete Ed25519 and SHA-256 soundness are audited assumptions, not cryptographic algorithms proved by those models.

Storage, serialization outside the modeled domain, deployment clocks, asynchronous orchestration, key custody, and tool behavior have their own qualification or assumption boundaries. A proved admission decision cannot establish that a later network delivery, database write, or external tool effect succeeded.

The manifest names every assumption the proofs inherit, and it admits exactly one Lean axiom beyond the standard ones: Chio.Json.hash_collision_resistant, the symbolic collision resistance registered as ASSUME-SHA256.

Read the required assumptions

formal/assumptions.tomltoml

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 and trusted computing base explains each dependency, such as ASSUME-ED25519 and ASSUME-SHA256. The formal overview describes the verification lanes and their artifacts.

Assess a claim from code to consequence

Trace each formal claim from its property to the runtime that relies on it:

Start with the property you rely on, and find it in the claim registry.
Locate its theorem or check, and confirm the modeled domain and the assumptions it inherits.
Follow the production caller that acts on the result, and confirm it uses the extracted decision.
Inspect the runtime and deployment evidence for every effect outside the proof.

Explore the proof and its runtime boundary

Formal overviewInspect the verification methods and their artifacts.Theorem inventoryLocate the named property and its claim class.Assurance modelConnect proof scope to the larger deployment trust boundary.Recovery after interruptionSee how runtime state carries decisions through failure.

PreviousVerifiable Evidence NextAssurance Boundaries & Limits