Runtime Verification presents Rust-to-Lean4 pipeline for zkEVM

A verification engineer at Runtime Verification explains a pipeline developed for the Ethereum Foundation to formally verify production Rust cryptographic libraries like Plonky3 and RISC Zero by translating them deterministically into Lean 4 mathematical models. The approach uses instruments like Aeneas and Hax alongside AI-assisted proof generation checked by the Lean kernel to ensure code matches specifications. The author notes that while AI significantly accelerates the proof process, engineers must carefully verify both specifications and intended optimizations to avoid false assurances. Open article →