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/postcondition propositions.

The toolchain is two-stage. Charon is a Rust front-end that emits a stable IR called LLBC. Aeneas then consumes LLBC and produces the proof-assistant output. Both are pinned in Chio CI; the pilot's promotion criteria require the pin to move deliberately:

schema = "chio.aeneas-pilot.v1"
status = "active_pilot"
owner = "formal-verification"
source = "formal/aeneas/verified_core.rs"
check_command = "./scripts/check-aeneas-pilot.sh"

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

The Pilot Lane

The pilot extracts a small set of functions chosen to fit the supported subset. The source is formal/aeneas/verified_core.rs: no external crates, no async, no unsafe, no heap allocation, no IO. This file mirrors the proof-facing shape of the Chio decision helpers and is used as the first extraction lane before promoting to production crate modules.

The full pilot file is short:

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 pilot checks that the pinned toolchain can extract this supported subset. It does not establish that other production Rust is extractable. The check command is ./scripts/check-aeneas-pilot.sh.

The Production Lane

The production lane extracts from this Chio module. Source: crates/kernel/chio-kernel-core/src/formal_aeneas.rs. Configuration:

schema = "chio.aeneas-production.v1"
status = "production_extraction"
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/AeneasEquivalence.lean"
artifact_report = "target/formal/aeneas-production/equivalence-artifacts.json"

extracted_symbols = [
  "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",
]

Fifteen extracted symbols model these decision helpers: time windows, scope-coverage flags, optional caps, monetary caps, budget commits, DPoP nonce admission, guard step composition, revocation denial, and receipt field coupling.

Extraction Flow

The extraction flow is:

• Rust source under chio-kernel-core/src/formal_aeneas.rs is written in a deliberately constrained subset (no async, no traits with associated types beyond what Aeneas supports, no heap allocation in extracted symbols).
• Charon translates the source to LLBC.
• Aeneas consumes LLBC and emits Lean 4 modules.
• The handwritten module Chio.Proofs.AeneasEquivalence imports the extracted output and proves equivalence to the handwritten model.
• The downstream proofs (in Proofs/Monotonicity.lean, Proofs/Evaluation.lean, depend on the handwritten model. The Aeneas equivalence theorems cover the listed extracted helpers; they do not establish equivalence for Rust outside formal_aeneas.rs.

Equivalence Theorems

Seven Aeneas equivalence theorems relate extracted definitions to handwritten definitions. They live in formal/lean4/Chio/Chio/Proofs/AeneasEquivalence.lean.

Each theorem is rootImported: true in the inventory and claimClass: aeneas_equivalence. The gate ./scripts/check-aeneas-equivalence.sh builds the equivalence module with lake build and confirms all seven theorems are proven without sorry.

P1: capability_monotonicity in this tool

P1 says a child capability's bounds are tighter than its parent's. Aeneas's contribution is mechanical: it extracts the bound-comparison helpers from the production Rust source so the downstream Lean equivalence theorem can compare extracted code against the handwritten model. The Rust function that drives P1 in production is ToolGrant::is_subset_of in crates/core/chio-core-types/src/capability/scope.rs, alongside ChioScope, ResourceGrant, and PromptGrant. Its bound-comparison helper, optional_u32_cap_is_subset, lives in the proof-facing helper module that Aeneas reads from.

That symbol is listed verbatim in the production extraction config:

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/AeneasEquivalence.lean"

extracted_symbols = [
  "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",
]

Three of those symbols carry P1 weight directly: optional_u32_cap_is_subset (invocation cap), monetary_cap_is_subset_by_parts (cost cap), and required_true_is_preserved (DPoP-required and similar boolean flags). The other extracted symbols cover P2, P3, P4, and P8 and are listed here because the Aeneas extraction is one config block per file; the per-symbol property attribution lives in the equivalence theorems that consume each extracted symbol.

The Aeneas-side mirror lives under the AeneasMirror namespace in Chio/Proofs/AeneasEquivalence.lean. For P1, the mirror is the optional-cap subset definition and its attendant equivalence theorem:

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

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 theorem says: if the parent has a cap and the Aeneas-extracted 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 boolean flags, simplifies the definition under each combination, and discharges the surviving goal directly from the subset hypothesis. The companion theorem for monetary caps, aeneas_monetaryCapIsSubset_preserves_parent_cap, has the same shape and is cited under the same P1 row in the inventory.

The bounded-model proofs in Proofs/Monotonicity.lean only know about the handwritten Lean definitions. The Aeneas equivalence theorems relate those proofs to the extracted helpers. A future change to optional_u32_cap_is_subset in the Rust source that altered its decision table would re-extract a different Lean definition, and aeneas_optionalCapIsSubset_preserves_parent_cap would either fail to elaborate or fail to prove. The gate ./scripts/check-aeneas-equivalence.sh runs inside the nightly proof report and again when a release is qualified; a divergence between the extracted and handwritten definitions fails those scheduled checks. Ordinary PR coverage is provided by the other configured gates.

Continue the tour at Kani Harnesses: P1 supporting harness or jump back to the P1 Tour.

Reproducing Locally

Run these three commands after installing the prerequisites. Charon, Aeneas, and Lean 4 each pin to a specific version under tools/.

# Lean toolchain pin (handled by lake)
cat formal/lean4/Chio/lean-toolchain
# leanprover/lean4:v4.28.0-rc1

# Pilot lane: extract verified_core.rs, build resulting Lean
./scripts/check-aeneas-pilot.sh

# Production lane: extract chio-kernel-core/src/formal_aeneas.rs
./scripts/check-aeneas-production.sh

# Equivalence: build the handwritten equivalence module
./scripts/check-aeneas-equivalence.sh

# Or: run the full Lean lane (every theorem in the inventory)
cd formal/lean4/Chio && lake build

Building Chio.Proofs.AeneasEquivalence
[7/7] proven without sorry
  proof.aeneas_timeWindowValid_equiv_model            OK
  proof.aeneas_optionalCapIsSubset_preserves_parent   OK
  proof.aeneas_budgetCommit_equiv_model               OK
  proof.aeneas_dpopAdmits_equiv_model                 OK
  proof.aeneas_revocationSnapshot_equiv_model         OK
  proof.aeneas_guardStep_equiv_model                  OK
  proof.aeneas_receiptCoupling_equiv_model            OK
EXITCODE: 0

The report at target/formal/aeneas-production/equivalence-artifacts.json records, per extracted symbol, the byte count of the LLBC, the line count of the resulting Lean, and the list of equivalence theorems that consume it.

Limits

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

• No async · The future monad is not part of the LLBC encoding. Extracted symbols must be 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.

These constraints explain why the manifest's excluded_surfaces list says: "Aeneas extraction from async, IO, SQLite, crypto, and string-heavy production modules outside crates/kernel/chio-kernel-core/src/formal_aeneas.rs". The Aeneas claim therefore covers only the functions listed in that file and configuration; the excluded modules remain a gap.

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 extracted_symbols in formal/aeneas/production.toml.
• Write a handwritten Lean model for the same logic in the appropriate file under Chio/Core/ or Chio/Proofs/.
• Add an equivalence theorem to Proofs/AeneasEquivalence.lean and a corresponding row to theorem-inventory.json.

Next

• 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.