Creusot Contracts

A postcondition defines what the returned value means

A requires annotation states a precondition and ensures states a postcondition. Creusot translates the annotated Rust into verification obligations for the Why3 proof platform, and a completed proof establishes the contract under its premises.

#[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 time-window postcondition says the returned Boolean equals issued_at ≤ now < expires_at. A false return is a valid answer for a time outside that interval: the contract defines the answer and leaves every input time admissible.

The specification language is Pearlite. Its @ operator projects a value into its logical view, so a machine integer becomes a mathematical integer for specification arithmetic. A sum in a ledger postcondition then describes the intended total without wrapping at the runtime type’s maximum. The Creusot tutorial explains the notation.

A budget commit deducts exactly and refuses without change

Start with two remaining invocations and nine units, and send requests that each cost one invocation and four units. Direct execution of the public budget_commit helper, in scalar accounting units, gives these results:

The contract states the general rule over u64 arguments: acceptance agrees with both costs fitting, acceptance subtracts each cost exactly, and refusal leaves both counters unchanged. The Kani budget harness checks a complementary property, counter monotonicity, over symbolic bytes widened to u64.

Both concern the pure decision. A shared spending authority also needs correct reservations, concurrency, and persistence, which Budgets & Metering explains.

The verifier reads the kernel’s own decision bodies

The isolated contract crate includes the kernel’s formal_aeneas.rs inside its aeneas_body module. Each registered wrapper states a contract and calls its declared function from that module, so the decision logic comes from the source file and the wrapper adds only the specification.

#[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");
}

The production source also carries specifications behind the chio_creusot_contracts cfg, which the core runner enables before cargo creusot prove. The isolated Cargo workspace depends on a pinned creusot-std revision, so the verifier compiles the contract crate and its included source without Chio’s runtime dependency graph.

The body-sync gate checks the include path, the allowed module shape, and the registered wrapper-to-function mapping. Each wrapper body must be the expected delegation call with its own parameters in order, so changed arguments or replacement logic fail it. The gate masks comments and strings first, then rejects conditional compilation in the contract crate, unexpected or nested functions, missing mappings, and missing production twins. Qualification: formal gates lists the gate and its source.

• Registry and body synchronization. The declared wrappers have the checked include and delegation shape.
• Toolchain smoke check. A generated diagnostic project proves with the installed tools, without exercising Chio’s contracts.
• Core solver check. The contract crate’s verification obligations complete under the selected toolchain and configuration.
• Runtime linkage review. The intended callers produce the relevant inputs and use the decision correctly in the wider system.

Only the solver check proves the postconditions. A postcondition replaced with ensures(true) still passes body synchronization, because the delegation body is unchanged, while a body replaced with true fails it. Review and the solver run establish what the contract says.

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)

Nine wrappers carry contracts for seven kinds of decision

The contract_twin entries name the exact wrapper and function pairs. Read each claim by the relationship its contract states:

• Time window. The result equals membership in the half-open validity interval.
• Budget precheck and commit. Acceptance needs both costs to fit; accepted costs are deducted, and rejected updates preserve the counters.
• Reservation ledger. Invalid updates preserve state; accepted reserves add their amount to the total; other accepted operations preserve the total; a finalized state stays unchanged.
• Invocation cap and required flag. An explicit parent cap requires a capped, no-larger child; a required parent flag requires the child flag.
• DPoP admission. When DPoP is required, admission requires present, valid, and nonce-fresh proof facts.
• Revocation snapshot. The denial result equals token-revoked or ancestor-revoked.
• Receipt coupling. The result equals the conjunction of the capability, request, verdict, policy-hash, and evidence-class match facts.

#[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)
}

A finalized ledger state has reserved at zero and at least one of committed, released, or retained nonzero. The theorem covers the scalar transition; store linkage, durable journal ordering, and concurrent reservation conservation sit outside it.

The registry’s covered_symbols list also names broader kernel symbols, and its goals include capability verification, scope resolution, and receipt signing. Those entries map subjects; a named runtime operation reaches a complete deductive refinement proof only through an annotated wrapper and its caller connection. The Rust verification aggregate requires the wrapper names in covered_symbols to agree with the contract_twin set.

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

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

The release records the metadata gate and the solver run separately

The two checks answer different questions. The metadata gate validates registry structure and body linkage without a solver. The core solver run proves the contract crate's obligations: Why3 dispatches each one to Alt-Ergo, Z3, cvc5, and cvc4, and the run passes when all 32 files prove. Both run before every release is tagged, and the proof report records each result against the tag's source commit.

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

The creusot line is the core solver result; a metadata-only pass never satisfies it. The contract dependency is pinned to Creusot revision a12f3ac7f688c7b93cee2c2eb60282004a2bdb30. To run either check from source, for example after changing a registered decision, follow Qualification: formal gates.

Each contract ends where its caller begins

The contract crate verifies the included decision source under its specification configuration. The runtime path decides when to call that decision and what effects follow, so Boolean facts still need correct producers, and numeric projections still need the right units, bounds, and ownership. Cryptography, storage, and external settlement rest on their own evidence and assumptions.

The methods strengthen one claim when their subjects connect. Aeneas relates generated Lean definitions to model statements, Kani checks selected harnesses with their inputs and compile configuration, and Lean makes the mathematical statement and its dependencies inspectable.

Next: the compiled harness behind the budget property