A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
Natalia Klaus, Juan Conejero, Palina Tolmach
cs.LO
May 28, 2026 · v2
TL;DR
Extracts production Rust cryptographic code into Lean 4 via Aeneas/Hax and proves correctness against ArkLib/CompPoly specs, with AI provers closing obligations.
Abstract
We describe a verification pipeline that takes production Rust cryptographic code and produces machine-checked correctness proofs in Lean 4. The pipeline combines three components: symbolic extraction tools (Charon and Aeneas, or Hax) that lift Rust into Lean 4; formal cryptographic specification libraries (ArkLib and CompPoly, from the Verified zkEVM project) that provide the mathematical targets; and AI provers (Aristotle from Harmonic AI and Aleph from Logical Intelligence) that close the resulting proof obligations. Every proof is checked by the Lean kernel, so AI output cannot compromise soundness. Within the scope of the Ethereum Foundation's zkEVM Verification Project, we applied the pipeline to cryptographic primitives in Plonky3 (FRI folding, Mersenne31 and KoalaBear field arithmetic, Horner polynomial evaluation) and RISC Zero (Merkle inclusion verification). In addition, Aleph authored proofs of two bounds-style theorems in Plonky3's compute_log_arity_for_round that previously stood as sorry. The paper describes the architecture, walks through a running example based on Aleph's two proofs, reports which classes of proof obligations AI closed and which required manual work, and discusses the engineering gaps we encountered: Lean 4 toolchain drift across tools and specific Aeneas/Hax extraction limits. We also document concrete missing lemmas, tactic gaps, and code-generation friction points discovered during proof development. We hope this contribution lowers the barrier to adoption of formal verification and facilitates more effective use of AI in this pipeline. The result is a working pipeline for formal verification of Rust, with kernel-checked proofs and reproducible artefacts.
Problem
Production Rust cryptographic code in zkVMs such as Plonky3 and RISC Zero needs correctness guarantees beyond testing. Existing Rust verifiers do not connect implementations to the abstract mathematical specifications that cryptographic protocols are defined against.
Approach
The pipeline lifts Rust into pure functional Lean 4 using Charon+Aeneas or Hax, and states theorems against formal specification libraries (ArkLib, CompPoly). Proof obligations are closed manually or by the AI provers Aristotle and Aleph. The Lean kernel re-checks every proof, so AI output cannot compromise soundness.
Results
The pipeline verified FRI folding and round scheduling, Mersenne31/KoalaBear field arithmetic, Horner evaluation, RISC Zero Merkle inclusion, and a 32-bit ADC. Aleph closed two previously sorry'd bounds theorems. AI handled control-flow, linear-arithmetic and simp-style obligations well. The report also documents engineering gaps, including Lean toolchain drift and extraction limits.
| Target | Pipeline | What was proved |
|---|
| Plonky3 FRI round-scheduling | Aeneas + Hax | 6 theorems; 2 closed by Aleph |
| Plonky3 arity-2 FRI fold | Aeneas + ArkLib | Matches abstract foldNth; no overflow in 13 checked ops |
| Plonky3 Horner evaluation | Hax + CompPoly | Evaluation correctness vs polynomial spec |
| RISC Zero Merkle inclusion | Hax | Root recomputation and inclusion-proof verification |
| 32-bit ADC | Hax + bv_decide | Bit-level correctness |
Selected verification targets (abridged from Table 1)
