Creusot Contracts

What Creusot does

A function annotated with #[requires(..)] and #[ensures(..)] is lowered to a Why3 verification condition. Chio's harness, configured in formal/rust-verification/creusot-core/why3find.json, names four provers in its provers array (alt-ergo, z3, cvc5, cvc4) and records a version and a timing for each in its profile array. Specifications are written in Pearlite, Creusot's specification language embedded in Rust attributes. The @ suffix visible below (now@, amount@) projects a Rust integer onto its logical view, a mathematical integer with no wraparound, so a spec can sum four ledger buckets and an incoming amount without the runtime type's finite width getting in the way.

Creusot has no extraction step, so there is nothing to keep in sync the way Aeneas's equivalence theorems keep an extracted Lean model aligned with handwritten Lean: the obligation is stated about the exact function annotated. That makes the whole guarantee turn on which function gets annotated, which is the question the rest of this page answers.

How it is wired

The registry is formal/rust-verification/creusot-contracts.toml, schema chio.creusot-contracts.v1, status core_contracts_required_for_strict_ci. The proof manifest registers the lane as creusot with posture required pointing at that file, and lists creusot in primary_toolchain, whose full value at the pin is lean4, creusot, kani, aeneas.

Its covered_symbols array concatenates two kinds of name. Twelve production chio_kernel_core symbols come first, then nine contract-function names prefixed by the crate path that holds them:

covered_symbols = [
  "chio_kernel_core::capability_verify::verify_capability",
  "chio_kernel_core::capability_verify::verify_capability_with_trusted",
  "chio_kernel_core::scope::resolve_matching_grants",
  "chio_kernel_core::scope::resolve_capability_grants",
  "chio_kernel_core::evaluate::evaluate",
  "chio_kernel_core::normalized::NormalizedToolGrant::is_subset_of",
  "chio_kernel_core::normalized::NormalizedResourceGrant::is_subset_of",
  "chio_kernel_core::normalized::NormalizedPromptGrant::is_subset_of",
  "chio_kernel_core::normalized::NormalizedScope::is_subset_of",
  "chio_kernel_core::normalized::NormalizedEvaluationVerdict::try_from_evaluation",
  "chio_kernel_core::receipts::sign_receipt",
  "chio_kernel_core::formal_core::revocation_snapshot_denies",
  "formal/rust-verification/creusot-core::time_window_valid_contract",
  "formal/rust-verification/creusot-core::budget_precheck_contract",
  "formal/rust-verification/creusot-core::budget_commit_contract",
  "formal/rust-verification/creusot-core::ledger_apply_conservation_contract",
  "formal/rust-verification/creusot-core::optional_u32_cap_subset_contract",
  "formal/rust-verification/creusot-core::required_true_preserved_contract",
  "formal/rust-verification/creusot-core::dpop_admits_contract",
  "formal/rust-verification/creusot-core::revocation_snapshot_denies_contract",
  "formal/rust-verification/creusot-core::receipt_fields_coupled_contract",
]

The goals the lane claims to establish are next, and the sixth is the one that describes the contract crate itself:

contract_goals = [
  "verify_capability returns success only for trusted issuer, valid signature, and valid time window",
  "scope matching is fail-closed for unsupported constraints and out-of-scope requests",
  "evaluate returns Allow only after capability, subject, scope, and guard checks pass",
  "normalized projections preserve every covered proof-facing field",
  "receipt signing refuses kernel-key mismatch before invoking the signing backend",
  "proof-facing Creusot wrappers verify single-sourced bodies included from formal_aeneas.rs",
  "reservation ledger transitions preserve amount totals, reject invalid updates unchanged, and make finalized states absorbing",
]

Single-sourced bodies

"Single-sourced bodies included from formal_aeneas.rs" is a literal description of the crate layout. The contract crate has exactly one module, and that module's entire content is a Rust include! of the production file:

#[allow(dead_code)]
mod aeneas_body {
    use creusot_std::{
        prelude::*,
        std::{clone::Clone, cmp::PartialEq, default::Default},
    };

    include!("../../../../crates/kernel/chio-kernel-core/src/formal_aeneas.rs");
}

crates/kernel/chio-kernel-core/src/formal_aeneas.rs is the pure, extraction-safe decision core. Its own header says the runtime-facing formal_core module calls these helpers and that inputs depending on strings, vectors, or runtime structs are projected to booleans or bounded integers before crossing the boundary. It carries its Creusot specifications inline, behind #[cfg_attr(chio_creusot_contracts, ensures(..))] at twenty sites, and crates/kernel/chio-kernel-core/Cargo.toml:100 registers that cfg so the production crate compiles clean without it. scripts/check-creusot-core.sh:17 is what turns the cfg on, by adding --cfg chio_creusot_contracts to RUSTFLAGS before cargo creusot prove.

Each wrapper in creusot-core/src/lib.rs states its contract and then delegates. The smallest one is four lines:

#[ensures(result == (issued_at@ <= now@ && now@ < expires_at@))]
pub fn time_window_valid_contract(now: u64, issued_at: u64, expires_at: u64) -> bool {
    aeneas_body::time_window_valid(now, issued_at, expires_at)
}

The largest states reservation-ledger conservation over four #[ensures] clauses: an invalid update returns the input state unchanged, a reserve operation adds its amount to the partition total, any other valid operation leaves the total fixed, and a state with no outstanding reservation and any non-zero terminal bucket is absorbing.

#[ensures(!result.1 ==> result.0 == state)]
#[ensures(result.1 && op@ == 0 ==>
    result.0.reserved@ + result.0.committed@ + result.0.released@ + result.0.retained@
        == state.reserved@ + state.committed@ + state.released@ + state.retained@ + amount@
)]
#[ensures(result.1 && op@ != 0 ==>
    result.0.reserved@ + result.0.committed@ + result.0.released@ + result.0.retained@
        == state.reserved@ + state.committed@ + state.released@ + state.retained@
)]
#[ensures(state.reserved@ == 0
    && (state.committed@ != 0 || state.released@ != 0 || state.retained@ != 0)
    ==> result.0 == state)]
pub fn ledger_apply_conservation_contract(
    state: ReservationLedger,
    op: u8,
    amount: u64,
) -> (ReservationLedger, bool) {
    aeneas_body::ledger_apply(state, op, amount)
}

formal/proof-manifest.toml:237 names this contract as one of four independent enforcement surfaces for reservation conservation, alongside bounded Apalache interleavings, a Kani harness, and a Lean witness over the same pure ledger_apply transition. The same note records the limit: the pure classifier and scalar admission are linked, and production ledger linkage is not established.

The gate that holds the shape

None of the arrangement above rests on discipline. scripts/check-creusot-body-sync.sh parses the contract crate and the production file with a Rust-aware masker that blanks comments and string literals, then refuses the build unless all of the following hold:

• The contract crate contains no cfg or cfg_attr attribute at all (check-creusot-body-sync.sh:270-273), so no contract can be compiled away.
• aeneas_body is the crate's only module, it is unconditional and top-level, and its body is exactly the allowlisted Creusot imports plus one include! (:274-328). The include path is matched against a literal regex naming crates/kernel/chio-kernel-core/src/formal_aeneas.rs.
• Every function in the crate ends in _contract, none is nested, and none is duplicated (:330-347).
• The set of contract functions and the set of [[contract_twin]] entries match in both directions, and every declared production twin exists as a top-level function in formal_aeneas.rs (:349-373).
• Each contract body is token-for-token the delegation call to its declared twin, passing that wrapper's own parameter names in order. Anything else is body drift.

for contract in sorted(contract_names):
    function = functions_by_name[contract]
    production = twins[contract]
    expected_call = f"aeneas_body::{production}({', '.join(function.parameters)})"
    expected_body = tokens(expected_call)
    if canonical_tokens(function.body) != canonical_tokens(expected_body):
        actual = " ".join(function.body)
        print("creusot-body-sync: BODY DRIFT", file=sys.stderr)
        print(
            f"  contract: {contract} (formal/rust-verification/creusot-core/src/lib.rs)",
            file=sys.stderr,
        )
        print(
            f"  twin:     {production} "
            "(crates/kernel/chio-kernel-core/src/formal_aeneas.rs)",
            file=sys.stderr,
        )
        print(f"  expected: {expected_call}", file=sys.stderr)
        print(f"  actual:   {actual}", file=sys.stderr)
        print("  The contract body must be exactly the expected delegation call.", file=sys.stderr)
        raise SystemExit(1)

A second gate compares the registry against itself. scripts/check-rust-verification-gates.sh:103-133 strips the formal/rust-verification/creusot-core:: prefix off covered_symbols and requires the resulting names to equal the [[contract_twin]] contract set exactly, reporting each direction of the difference by name. A contract added to the crate and forgotten in the toml fails, and so does the reverse.

What it covers

Nine contracts, nine declared twins. The pairs are the [[contract_twin]] tables at formal/rust-verification/creusot-contracts.toml:41-75:

The twins are the same functions the other lanes reason over. formal_core.rs wraps seven of the nine one call deep (budget_precheck at formal_core.rs:108-120, revocation_snapshot_denies at :311-313, and five more alongside), Aeneas extracts the file into Lean, and the Kani public harnesses execute it symbolically.

How far each predicate travels from there varies, and the page's claim stops where the call graph does. Two of the nine reach the normalized projection inside the kernel core: optional_u32_cap_is_subset at crates/kernel/chio-kernel-core/src/normalized.rs:127 and :178, and required_true_is_preserved at :156 and :201. One reaches the kernel crate: receipt_fields_coupled, through the crate re-export at crates/kernel/chio-kernel/src/receipt_support/coupling.rs:41. The time-window path enters formal_aeneas.rs through a different door: production calls formal_core::classify_time_window (capability_verify.rs:43), which calls formal_aeneas::classify_time_window_code, while the boolean formal_core::time_window_valid the contract shadows carries #[allow(dead_code)] at formal_core.rs:32. The remaining twins are reached by the proof lanes and the harnesses rather than by a production call site.

The contract crate itself is isolated. Its Cargo.toml declares its own empty [workspace] outside Chio's main one, with a single dependency, creusot-std, pinned to a git revision. The pinned Creusot toolchain therefore compiles this small crate plus the included production file, not Chio's full dependency graph.

Relation to the other lanes

Four lanes reach formal_aeneas.rs, and they reach it differently. Aeneas mechanically extracts it via Charon into Lean and pairs each function with a generated equivalence theorem. Kani's public harnesses live inside chio-kernel-core and execute the functions symbolically up to a bounded unwind. Lean hand-writes an independent model in a different logic and proves the abstract properties there. Creusot proves deductive contracts over the same text, compiled with the specification cfg on, for every input the argument types admit.

The manifest marks both Creusot and Kani required for Rust refinement; Aeneas splits into separate pilot and production lanes. No lane stands alone: the property matrix draws on more than one per property, so no single lane's blind spot defines the claim.

Reproduce

The registry and body-sync checks need no verification toolchain. They run in the pull-request lane at .github/workflows/formal-pr-smoke.yml:358-364 with CHIO_RUST_VERIFICATION_METADATA_ONLY set, which is why check-creusot-body-sync.sh runs at check-rust-verification-gates.sh:136, before the metadata-only exit at :138-141. Body drift fails on every matching pull request; the solver run does not.

# Registry shape plus the body-sync gate. No toolchain required.
CHIO_RUST_VERIFICATION_METADATA_ONLY=1 ./scripts/check-rust-verification-gates.sh

# Toolchain canary, then the real proof.
./scripts/check-creusot-smoke.sh
./scripts/check-creusot-core.sh

On success the metadata-only run prints two lines. The first comes from the body-sync gate at check-creusot-body-sync.sh:397-399 and the second from the early exit at check-rust-verification-gates.sh:139:

creusot-body-sync: all contract bodies delegate to their declared production twins
Rust verification gate metadata passed; strict Creusot/Kani execution explicitly disabled

Dropping the environment variable runs the strict lane, which needs both Creusot and Kani on PATH and exits non-zero without them. check-creusot-smoke.sh is a toolchain canary: it scaffolds a disposable cargo creusot new project pinned to the same revision and proves it, which shows nothing about Chio's logic, only that the toolchain still works. check-creusot-core.sh runs cargo creusot prove inside the contract crate. Per-solver timings are recorded in the profile array of creusot-core/why3find.json:10-15: cvc5 at 0.473 seconds, z3 at 0.165, alt-ergo at 0.232, and cvc4 at 0.506. No captured output for the strict lane accompanies this page, because it needs the pinned Creusot install.

The strict path reaches CI through the workspace proof report. .github/workflows/nightly.yml:372-392 installs Creusot from its pinned revision, and :404-418 unsets the metadata-only variable, generates the report, and fails the job unless its mode is strict. .github/workflows/release-qualification.yml:168-174 installs the same pinned revision.

Limits

• Projected inputs · every twin takes booleans and bounded integers. The projection from strings, vectors, and runtime structs down to those arguments happens in normalized.rs and capability_verify.rs and is outside every contract on this page.
• The wrapper, not the call site · a green run proves the nine annotated functions satisfy their postconditions over the included bodies. It says nothing about the kernel binary, the storage layer, or any caller that decides when to consult these predicates.
• Cryptography stays assumed · none of these contracts touch Ed25519 or SHA-256. See Assumptions and TCB.
• The solver run is not a per-pull-request gate · the body-sync and registry checks are. The proof itself runs where the toolchain is installed.

Next

• Aeneas Pipeline · the extraction lane over the same file.
• Kani Harnesses · the other required strict-CI Rust refinement lane.
• Verified Core Boundary · which Rust names the proof boundary covers, and what being listed entitles a claim to say.