Aeneas: Rust to Lean, F* and Rocq translation via Charon
========================================================

Aeneas translates Rust into pure functional models for Lean, F* or Rocq through the Charon frontend. A May 2026 pipeline paper used it with hax, ArkLib and CompPoly, plus AI provers, to verify Plonky3 FRI folding and field arithmetic and RISC Zero Merkle checks.

Maintainer: Inria (Son Ho) and AeneasVerif
Website: https://github.com/AeneasVerif/aeneas
Category: Verified implementations
Targets: Rust, Plonky3 and RISC Zero code (2026 pipeline paper)
Approach: Functional translation of Rust into pure models for Lean, F* or Rocq
Access: Open source
Status: Active
Strengths: Lean-first, integrates with ArkLib and Clean. | Demonstrated on real prover code. | Handles ownership-heavy Rust well.
Limits: Rust subset limitations. | Translation is in the TCB. | Younger than hax in production use.
Firms using it: none listed
Sources: https://github.com/AeneasVerif/aeneas | https://arxiv.org/abs/2605.30106

Source page: https://sorryfree.com/frameworks/aeneas/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13