From Production Rust to Lean 4 Proofs: A Verification Pipeline

A working pipeline from production Rust cryptographic code to kernel-checked Lean 4 proofs, built within the Ethereum Foundation's zkEVM Verification Project. Charon lowers Rust to a typed IR, Aeneas translates it to pure-functional Lean 4, and we prove the extracted code against formal specs from ArkLib and CompPoly.

Closed so far: the arity-2 FRI fold step in Plonky3 matches a pure spec, never panics, no overflow (0 sorry). Also FRI round scheduling, Mersenne31 and KoalaBear field arithmetic, RISC Zero Merkle inclusion, 32-bit ADC via bv_decide. Two polynomial-algebra theorems connecting to ArkLib's foldNth remain open, and we show why they are hard.

Running example: Aleph authored proofs of two bounds theorems that stood as sorry. Every AI proof is re-checked by the Lean kernel, so soundness never depends on the AI. We cover where AI provers help, where they fail, and the toolchain friction to budget for.

Code: github.com/Verified-zkEVM/rust-lean.

Preprint: arXiv:2605.30106.

Speakers: Natalia Klaus

Track: Security