Aeneas Pipeline

What Aeneas does

Aeneas takes Rust source and produces a translation in a proof assistant. The translation excludes effectful code (async, IO, unsafe blocks) and represents the remaining pure logic as functional definitions plus pre and postcondition propositions.

The toolchain is two-stage. Charon is a Rust front-end that emits a stable IR called LLBC. Aeneas consumes LLBC and emits the proof-assistant output. Both are pinned by content hash per architecture in formal/aeneas/production.toml, and the equivalence gate refuses to run if the binaries on disk do not hash to the declared values.

The pilot lane

The pilot registry is:

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

Two fields are worth reading closely. Its status is toolchain_upgrade_fixture, and its purpose says in the registry's own words that it is a Minimal extraction fixture retained for Aeneas and Charon toolchain-upgrade diagnosis; production evidence comes from the production lane. The pilot is a diagnostic, not a staging area, and no property row cites it.

Its source is formal/aeneas/verified_core.rs: no external crates, no async, no unsafe, no heap allocation, no IO. The whole file is short enough to read at once:

#![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 gate is ./scripts/check-aeneas-pilot.sh, which extracts this file and fails if the generated Lean is missing the Decision type. A clean run prints Aeneas pilot check passed.

The production lane

The production lane extracts from two registered Rust sources and compares the result against a committed snapshot. Its header:

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

Three things in that header set the shape of everything below. The status is generated_equivalence, so the theorems are stated over generated definitions rather than over transcriptions of them. The equivalence_module is Proofs/AeneasGeneratedEquivalence.lean, not the handwritten Proofs/AeneasEquivalence.lean beside it. And generated_snapshot names two committed Lean files, so a re-extraction that produces different output fails a snapshot comparison rather than silently replacing the input to the proofs.

The registry declares two [[sources]] tables: kernel_core, which is crates/kernel/chio-kernel-core/src/formal_aeneas.rs, and economy_conversion, which is crates/economy/chio-credit/src/formal_economy.rs. It then declares four [[targets]] tables over those sources, each pairing a list of functions with a list of equivalence theorems one to one:

The decision_core target carries the capability and admission helpers:

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

The manifest scopes what this lane reaches at formal/proof-manifest.toml:240, in its own words: production extraction pairs every registered decision-core, reservation-ledger, Merkle-walk and economy-conversion function with a generated Lean equivalence theorem; the economy evidence proves scalar ceil and floor rounding only, with collection conservation and production netting absorption left outside it; and the ledger theorem reaches the bounded transition model while concrete runtime store linkage remains outside it.

Extraction flow

• Each registered source is written in a constrained subset: no async, no IO, no heap allocation in the extracted symbols.
• Charon translates the source to LLBC.
• Aeneas consumes LLBC and emits Funs.lean and Types.lean under the target's work directory.
• scripts/snapshot-aeneas-generated.sh --check compares that output against the committed snapshot under formal/lean4/Chio/FormalAeneas and FormalEconomy.
• Chio.Proofs.AeneasGeneratedEquivalence imports the snapshot and proves each registered function equal to a handwritten mirror, then derives the property theorems from that equality.
• The downstream proofs in Proofs/Monotonicity.lean and Proofs/Evaluation.lean are stated over the handwritten model. The equivalence theorems are what connect them to the extracted code, and they connect nothing outside the registered targets.

The equivalence theorems

formal/theorem-inventory.json registers 32 theorems with claimClass: aeneas_equivalence, split across two modules: 25 in the generated module Proofs/AeneasGeneratedEquivalence.lean and 7 in the handwritten Proofs/AeneasEquivalence.lean. Every one is rootImported: true.

The handwritten module carries the mirror definitions plus the derivations the generated theorems reduce to. The 7 registered ones are:

That module declares fourteen theorems in total, so seven of them are unregistered: the two wildcard-coverage theorems, the prefix-wildcard one, aeneas_requiredTrueIsPreserved_equiv, aeneas_monetaryCapIsSubset_preserves_parent_cap, aeneas_budgetPrecheck_equiv_model and aeneas_nonceAdmits_equiv_model. They elaborate in the same build and no property row cites any of them, so they are not evidence for anything under the manifest's own rule at formal/proof-manifest.toml:238: Lean assets are release evidence only when root-imported, sorry-free and mapped to a property-matrix entry.

P1 in this lane

P1 is capability attenuation: a delegated capability can only narrow. The Aeneas contribution is mechanical. It extracts the bound-comparison helpers from the shipped Rust so a Lean theorem can be stated over the extracted definition rather than over a transcription of it. Three functions in the decision_core target carry P1 weight: optional_u32_cap_is_subset (invocation cap), monetary_cap_is_subset_by_parts (cost caps) and required_true_is_preserved (the DPoP-required flag).

The handwritten mirror for the first of those is:

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

The theorem stated over it, which the inventory registers as proof.aeneas_optionalCapIsSubset_preserves_parent_cap with mapsTo: ["P1"]:

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

If the parent has a cap and the subset check accepts, then the child must also have a cap and its value must be bounded by the parent's. The proof case-splits on the two booleans, simplifies the definition under each combination, and discharges the surviving goal from the subset hypothesis.

That theorem is a bridge, not the evidence P1's row cites. The row names proof.generated_optional_u32_cap_is_subset_preserves_parent_cap in the generated module, and the inventory records the relationship in its own note on the handwritten one: it is a Derived ordinary-value attenuation bridge whose generated-code successor is the theorem the row cites. The generated theorem is stated over Chio.AeneasProduction.optional_u32_cap_is_subset returning ok true, rewrites through the generated-to-mirror equality, and then applies the handwritten bridge. The P1 tour quotes it in full.

The monetary-cap counterpart aeneas_monetaryCapIsSubset_preserves_parent_cap has the same shape and is one of the seven theorems the inventory does not register, so it backs no property row.

What this lane does not reach: the proofs in Proofs/Monotonicity.lean are stated over the handwritten Lean definitions, and the equivalence theorems are the only thing tying them to shipped Rust. A change to optional_u32_cap_is_subset that altered its decision table would re-extract a different Lean definition, and the generated theorem would fail to prove. A change to any Rust the registry does not list would be invisible here.

Reproduce

The lane needs Lean and lake plus the pinned Charon and Aeneas binaries. scripts/install-aeneas-toolchain.py fetches them and writes an install receipt; the production check refuses to run without one.

# The Lean toolchain pin lake uses
cat formal/lean4/Chio/lean-toolchain

# Fetch and authenticate the pinned Charon and Aeneas binaries
./scripts/install-aeneas-toolchain.py

# Pilot lane: extract formal/aeneas/verified_core.rs
./scripts/check-aeneas-pilot.sh

# Production lane: extract both registered sources, snapshot-check the
# output, then run the equivalence gate
./scripts/check-aeneas-production.sh

# The equivalence gate on its own
./scripts/check-aeneas-equivalence.sh

The last of those does the work worth knowing about. In order, it snapshot-checks the generated Lean against the committed copy, then checks that CHIO_AENEAS_RELEASE_TAG appears exactly once in each of nightly.yml and release-qualification.yml and agrees with both the registry and the vendor manifest, hashes every vendored Aeneas file and compares the digest against content_sha256, rejects a vendored Lean file containing sorry, requires every declared theorem in the equivalence module to have a matching #print axioms line, requires every equivalence_theorems row to resolve to one of those declarations, requires the module to be root-imported exactly once from Chio.lean and to appear in the manifest's root_modules, and finally elaborates the module and fails on sorryAx or a declaration with metavariables in the build log. A clean run prints Aeneas generated equivalence gate passed.

It writes target/formal/aeneas-production/equivalence-artifacts.json as it goes: a SHA-256 for every input it considered, the vendor release tag and content hash, the toolchain report, the registered targets with their functions and types, and the resolved symbol-to-theorem map.

Limits

Aeneas does not handle all of Rust. The main constraints visible in the Chio extraction are:

• No async · Rust's async encoding is not part of LLBC. Every extracted symbol is synchronous.
• No IO or syscalls · File handles, sockets, and timers are excluded. The pure decision core is the only thing in scope.
• Limited trait support · Extracted code uses traits sparingly and prefers concrete types or enums over generic interfaces. The pilot file's Decision enum is a worked example.
• No heap allocation in extracted symbols · The production lane extracts numeric and boolean helpers; string-heavy or vec-heavy code stays out of the lane.
• Bounded recursion · Recursion that the termination checker cannot establish needs a manual termination proof; the Chio extraction prefers iteration where it can.

The manifest states the boundary those constraints produce in its excluded_surfaces list at formal/proof-manifest.toml:223: Aeneas extraction from async, IO, SQLite, crypto, and string-heavy production modules outside the registered sources in formal/aeneas/production.toml. The registered sources are the boundary, not one file.

Extending the extraction

Adding a new extracted symbol to the production lane is a four-step PR:

• Write the function in crates/kernel/chio-kernel-core/src/formal_aeneas.rs using the constrained subset described above.
• Add the symbol to the functions list of the relevant [[targets]] table in formal/aeneas/production.toml, and add its equivalence_theorems row. The gate rejects a target whose two lists differ in length.
• Write a handwritten Lean model for the same logic in the appropriate file under Chio/Core/ or Chio/Proofs/.
• Add the equivalence theorem to Proofs/AeneasGeneratedEquivalence.lean with a matching #print axioms line, and a row in theorem-inventory.json. Without the inventory row and a property-matrix citation the theorem elaborates but is evidence for nothing.

See also

• Theorem Inventory · the full table including the seven Aeneas equivalence theorems.
• Lean 4 Proofs · the proof structure that consumes the equivalence theorems.
• Kani Harnesses · the bounded model-checking lane that runs alongside Aeneas.