2026-11-05 –, Lotus Stage 2
Production Rust from Plonky3 and RISC Zero, turned into machine-checked Lean 4 proofs. AI provers close proof obligations, the Lean kernel re-checks every step. You leave with a realistic picture of what Rust-to-Lean verification delivers today, what it costs, and how AI provers change the economics.
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.
Natalia Klaus is a verification engineer at Runtime Verification, where she works on formal verification of Linux kernel code in Rust and C. She builds the Rust-to-Lean 4 pipeline (Charon, Aeneas) and uses AI provers to close proof obligations within the Ethereum Foundation's zkEVM Verification Project, with verified targets including Plonky3 FRI folding and RISC Zero Merkle inclusion. Previously she verified the Tezos OCaml codebase at Formal Land. She holds a Master's degree in Systems Analysis from Southern Federal University, with a focus on lambda calculus, mathematical logic and category theory.