Rust to Lean 4 Proof Verification Pipeline by Ethereum Foundation

The Ethereum Foundation's zkEVM Verification Project presents a working verification pipeline from production Rust cryptographic code to kernel-checked Lean 4 proofs. Presented by Natalia Klaus, the pipeline uses Charon to lower Rust to a typed IR, Aeneas to translate it to pure-functional Lean 4, and proves the extracted code against formal specifications from ArkLib and CompPoly. Completed verification steps include the arity-two FRI fold step in Plonky3 matching a pure spec with no panics or overflow, FRI round scheduling, Mersenne31 and KoalaBear field arithmetic, RISC Zero Merkle inclusion, and 32-bit ADC via bv_decide. Two polynomial-algebra theorems connecting to ArkLib's foldNth remain open. Additionally, the project covers AI-authored proofs of bounds theorems where every AI proof is re-checked by the Lean kernel, ensuring soundness does not depend on the AI, while highlighting where AI provers help or fail alongside toolchain friction.