Aeneas Pipeline

Trace a registered Rust decision through authenticated extraction into Lean, and check the theorem that relates it to the model.

On this page

For each registered Rust decision helper, a Lean theorem relates the definition Aeneas extracts from the source to Chio's handwritten model.

Charon and Aeneas translate two registered sources, holding four target groups of synchronous numeric and Boolean decisions, into committed Lean snapshots. A fresh extraction must match those snapshots byte for byte before the equivalence module builds, so the code that makes the decision is itself an input to the proof.

Aeneas pipelineChoose a check.

A theorem relates generated definitions to the model

For optional_u32_cap_is_subset, the generated theorem states: if the computation returns ok true and the parent has a cap, the child has a cap at or below it. The gate elaborates the equivalence module and rejects sorryAx in its output. P1 extraction.

Source

formal/aeneas/production.tomlformal/lean4/Chio/Chio/Proofs/AeneasGeneratedEquivalence.lean

Authenticated extraction for the two registered sources and their four target groups. Matching bytes detects drift, and the equivalence theorem states the semantic relationship; async, IO, SQLite, cryptographic, and string-heavy modules sit outside the registered sources.

Extraction produces the definition, and the theorem relates it to the model

Charon reads the registered Rust source and produces an intermediate representation called LLBC. Aeneas translates LLBC into Lean function and type definitions, which Chio commits in FormalAeneas and FormalEconomy so the proof build has inspectable inputs.

The equivalence theorem does a different job. It states a relationship between that generated definition and the handwritten model, including the conversion from machine values to mathematical values. The proof module imports the generated definitions alongside Chio's handwritten modules.

The production gate authenticates the installed Charon and Aeneas binaries against the registered hashes and installation receipt, extracts each registered source, and calls the equivalence gate. That gate checks both snapshot directories, validates the vendor and registry bindings, then builds and elaborates the equivalence module.

Two sources register four target groups

The production registry names two source files and four target groups. Each group concentrates rules that the surrounding Rust calls.

Target group	Decisions	Source
`decision_core`	Time windows, caps, required flags, budgets, DPoP, nonces, revocation, guards, receipt coupling	`formal_aeneas.rs`
`reservation_ledger`	Terminal-state classification and one ledger transition	`formal_aeneas.rs`
`merkle_walk`	One inclusion-walk step: sibling use, side, next index and size	`formal_aeneas.rs`
`economy_conversion`	Scalar ceil and floor conversion	`formal_economy.rs`

The first three groups come from the kernel core's formal_aeneas.rs, and conversion from chio-credit's formal_economy.rs. The registry maps each listed function to its generated equivalence theorem, and the gate checks the symbol sets, required types, and theorem declarations.

Inspect the production and pilot registrations

formal/aeneas/production.toml1-17toml

schema = "chio.aeneas-production.v1"
status = "generated_equivalence"
owner = "formal-verification"
source = "crates/kernel/chio-kernel-core/src/formal_aeneas.rs"
command = "./scripts/check-aeneas-production.sh"
equivalence_command = "./scripts/check-aeneas-equivalence.sh"
equivalence_module = "formal/lean4/Chio/Chio/Proofs/AeneasGeneratedEquivalence.lean"
artifact_report = "target/formal/aeneas-production/equivalence-artifacts.json"
negative_registry = "formal/aeneas/negative-tests.toml"
vendor_manifest = "formal/lean4/vendor/aeneas/VENDOR.toml"
vendor_release_tag = "build-2026.04.22.215158-38d10a22642d75d051e14006cc6e45055381f10e"
snapshot_layout = "emitted_module_path"
snapshot_normalization = "identity"
generated_snapshot = [
  "formal/lean4/Chio/FormalAeneas/Funs.lean",
  "formal/lean4/Chio/FormalAeneas/Types.lean",
]

formal/aeneas/production.toml62-100toml

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

formal/aeneas/pilot.tomltoml

schema = "chio.aeneas-pilot.v1"
status = "toolchain_upgrade_fixture"
owner = "formal-verification"
source = "formal/aeneas/verified_core.rs"
check_command = "./scripts/check-aeneas-pilot.sh"
production_lane = "formal/aeneas/production.toml"
purpose = "Minimal extraction fixture retained for Aeneas and Charon toolchain-upgrade diagnosis; production evidence comes from the production lane."

extracted_symbols = [
  "time_window_valid",
  "dpop_subset",
  "budget_precheck",
  "governed_approval_passes",
  "evaluate_signature_time_scope",
  "report_may_use_verified_label",
]

promotion_criteria = [
  "Charon and Aeneas versions are pinned together in CI",
  "Aeneas extracts the pure chio-kernel-core decision modules without unsupported Rust features",
  "Generated Lean imports are compared against the handwritten Chio.Core and Chio.Proofs modules",
  "Any missing external model is listed in formal/assumptions.toml or added as an Aeneas Lean model",
]

formal/aeneas/verified_core.rsrust

#![allow(dead_code)]

// Aeneas pilot source for pure Chio decision functions.
//
// This file intentionally avoids external crates, async code, unsafe code,
// heap allocation, and IO so Charon/Aeneas can extract a Lean model. It mirrors
// the proof-facing shape of chio-kernel-core decisions.

pub enum Decision {
    Allow,
    Deny,
}

pub fn time_window_valid(now: u64, issued_at: u64, expires_at: u64) -> bool {
    issued_at <= now && now < expires_at
}

pub fn dpop_subset(parent_required: bool, child_required: bool) -> bool {
    !parent_required || child_required
}

pub fn budget_precheck(
    remaining_invocations: u64,
    remaining_units: u64,
    invocation_cost: u64,
    unit_cost: u64,
) -> bool {
    invocation_cost <= remaining_invocations && unit_cost <= remaining_units
}

pub fn governed_approval_passes(approval_required: bool, approval_token_valid: bool) -> bool {
    !approval_required || approval_token_valid
}

pub fn evaluate_signature_time_scope(
    signature_valid: bool,
    scope_match: bool,
    now: u64,
    issued_at: u64,
    expires_at: u64,
) -> Decision {
    if !signature_valid {
        Decision::Deny
    } else if !time_window_valid(now, issued_at, expires_at) {
        Decision::Deny
    } else if !scope_match {
        Decision::Deny
    } else {
        Decision::Allow
    }
}

pub fn report_may_use_verified_label(label: u8) -> bool {
    label == 2
}

The generated cap check keeps a child within its parent's cap

The invocation-cap helper decides whether a proposed child cap fits its parent. With a parent cap of 10, a child cap of 4 passes, and 11 or an absent child cap fails. The generated theorem states the general result over machine values: if the computation returns ok true and the parent has a cap, the child has a cap at or below it.

\mathtt{optional\_u32\_cap\_is\_subset}(\ldots) = \mathrm{ok\ true} \;\wedge\; \htmlClass{cor-parent}{p_{\mathrm{has}}} \;\Longrightarrow\; \htmlClass{cor-child}{c_{\mathrm{has}}} \wedge \htmlClass{cor-child}{c} \htmlClass{cor-relation}{\le} \htmlClass{cor-parent}{p}

Four objects carry the argument:

Generated computation. optional_u32_cap_is_subset takes Boolean presence flags and U32 values; the theorem's premise requires the result ok true.
Generated-to-mirror equality. Relates that computation to optionalCapIsSubset on the natural-number projections of the U32 values.
Ordinary-value bridge. An accepted mirror result and a present parent cap imply a present, bounded child cap.
Generated property theorem. Rewrites through the equality, obtains the accepted mirror result, and applies the bridge.

Read the generated theorem

formal/lean4/Chio/Chio/Proofs/AeneasGeneratedEquivalence.lean802-813lean

theorem generated_optional_u32_cap_is_subset_preserves_parent_cap
    (childHasCap parentHasCap : Bool)
    (childValue parentValue : U32)
    (subsetGenerated :
      Chio.AeneasProduction.optional_u32_cap_is_subset
        childHasCap childValue parentHasCap parentValue = ok true)
    (parentPresent : parentHasCap = true) :
    childHasCap = true ∧ childValue.val <= parentValue.val := by
  rw [generated_optional_u32_cap_is_subset_eq_mirror] at subsetGenerated
  injection subsetGenerated with subsetMirror
  exact aeneas_optionalCapIsSubset_preserves_parent_cap
    childHasCap parentHasCap childValue.val parentValue.val subsetMirror parentPresent

formal/lean4/Chio/Chio/Proofs/AeneasEquivalence.lean32-37lean

def optionalCapIsSubset
    (childHasCap : Bool)
    (childValue : Nat)
    (parentHasCap : Bool)
    (parentValue : Nat) : Bool :=
  !parentHasCap || (childHasCap && childValue <= parentValue)

formal/lean4/Chio/Chio/Proofs/AeneasEquivalence.lean116-124lean

theorem aeneas_optionalCapIsSubset_preserves_parent_cap
    (childHasCap parentHasCap : Bool)
    (childValue parentValue : Nat)
    (h_subset :
      AeneasMirror.optionalCapIsSubset childHasCap childValue parentHasCap parentValue = true)
    (h_parent : parentHasCap = true) :
    childHasCap = true ∧ childValue <= parentValue := by
  cases childHasCap <;> cases parentHasCap <;> simp [AeneasMirror.optionalCapIsSubset] at h_subset h_parent ⊢
  exact h_subset

The result gives scalar attenuation an implementation connection. Complete scope refinement also needs the other grant fields, grant kinds, projections, and callers; the P1 walkthrough separates that larger claim from this statement.

AeneasEquivalence.lean holds handwritten ordinary-value definitions and their bridges. AeneasGeneratedEquivalence.lean imports the generated snapshots and proves statements over their definitions. The inventory's aeneas_equivalence class includes entries from both, so read the source module to tell a mirror fact from a statement over generated Rust.

Filter aeneas_equivalence or search an exact theorem name in the Theorem Inventory, then inspect the entry's source module, premises, property mapping, and notes. An entry and its rootImported flag are registry declarations; a passing build is separate evidence.

The release you run carries the extraction result

The production extraction lane runs before every release is tagged. It extracts both registered sources, checks their snapshots byte for byte, and builds the generated equivalence module; it passes only after every nested check passes. The proof report records the lane's result against the tag's source commit, and the release workflow signs it. Check it for the binary on your PATH:

Terminalbash

chio release verify --evidence formal

Output

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 aeneas line is this lane. The report also binds equivalence-artifacts.json, which records the input hashes, snapshots, vendor, toolchain, and registered targets the extraction used. The pilot fixture, registry status toolchain_upgrade_fixture, isolates a Charon or Aeneas upgrade and contributes no production evidence.

To run the lane from source, for a toolchain upgrade or a new registered decision, follow Qualification: formal gates. The registered extraction binaries target Linux x86_64 and aarch64.

Understand the snapshot and proof checks

The equivalence gate calls snapshot-aeneas-generated.sh --check for each source with explicit generated and snapshot directories. Without directory overrides the helper checks only its default kernel snapshot, and without --check it writes snapshots, so verify through the gate.

The gate also binds the registered release tag to the workflow and vendor declarations, validates the vendored content and imports, and checks declared theorem coverage and the required root import. It then builds and elaborates AeneasGeneratedEquivalence.lean, which prints the axioms of its declared theorems, and scans the log for sorryAx, incomplete declarations, and metavariables before reporting success. The broader Lean gate audits project assumptions and module imports.

A theorem here covers the registered decisions, and the code around them has its own evidence

The registered sources concentrate synchronous numeric and Boolean decisions. The manifest keeps async, IO, SQLite, cryptographic, and string-heavy production modules outside them; that is Chio's declared extraction scope, separate from what Aeneas supports in general. Servers, storage engines, and cryptographic libraries around the declared functions rest on other evidence.

A scalar theorem still needs correct callers, input projection, and interpretation of its result. A ledger transition needs its linkage to a durable runtime store, a Merkle step the complete proof parser and hashing path, and conversion the surrounding economic accounting, where collection conservation and netting carry their own evidence. The assumption register and property-specific evidence follow those obligations.

When a registered decision changes, fresh extraction can fail snapshot comparison first. Reviewing the snapshot and rechecking that the theorem proves the intended statement are separate steps. Extending the lane takes four:

Register. Choose a registered source, or extend the source registry explicitly, and add the function, its required types, and its target mapping.
State. Write the generated equivalence theorem, review the new snapshots, state the relationship to the model, and import the proof module.
Map. Add the inventory and property mappings the claim requires.
Run. Run the production extraction and complete Lean gates with the matching toolchain, and retain their results beside the implementation linkage and any runtime checks the claim needs. Failure Modes explains drift, missing inputs, and proof failures.

Next: read the statements the generated code meets

Lean 4 ProofsRead the model statements, premises, and the one approved axiom.P1: Capability MonotonicityFollow one property across its Lean, Aeneas, Kani, and differential evidence.Formal QuickstartCheck the formal evidence your release carries.

PreviousLean 4 Proofs NextCreusot Contracts