A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
Natalia Klaus, Palina Tolmach, Juan Conejero
cs.LO
May 28, 2026 · v1
TL;DR
Pipeline lifts Rust crypto code into Lean 4 and closes correctness proofs with AI provers, kernel-checked.
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
Formal verification of production Rust cryptographic code has historically required enormous manual effort, and no prior pipeline connected production Rust to abstract mathematical specifications with machine-checked proofs at scale.
Approach
The pipeline combines symbolic extraction tools (Charon/Aeneas and Hax) that lift Rust into pure functional Lean 4, formal cryptographic specification libraries (ArkLib and CompPoly), and AI provers (Aristotle from Harmonic AI and Aleph from Logical Intelligence) that close proof obligations. Every proof is checked by the Lean kernel, so AI output cannot compromise soundness.
Results
The pipeline verified cryptographic primitives in Plonky3 (FRI folding, Mersenne31/KoalaBear field arithmetic, Horner evaluation) and RISC Zero (Merkle inclusion verification). Aleph closed two bounds-style theorems in Plonky3's compute_log_arity_for_round that previously stood as sorry. AI provers handled control-flow lemmas, linear arithmetic, and simp-closeable boilerplate reliably.
| Target | Pipeline | What was proved |
|---|
| Plonky3 FRI round-scheduling | Aeneas + Hax | 6 theorems incl. bounds, monotonicity; 2 closed by Aleph |
| Plonky3 arity-2 FRI fold | Aeneas + ArkLib | Rust matches abstract foldNth; no overflow across 13 ops |
| Plonky3 Mersenne31 field arithmetic | Aeneas | Addition and multiplication of the Rust model |
| Plonky3 Horner evaluation | Hax + CompPoly | Evaluation correctness against polynomial spec |
| RISC Zero Merkle inclusion | Hax | Root recomputation and inclusion-proof verification |
Verification targets under the zkEVM Verification Project
