Mar 25
Loading video player...
Episode 396. Aired on Mar 25, 2026 See full episode on https://zeroknowledge.fm/podcast/396/ zkMesh+ is live! Subscribe for zkMesh+ and catch the latest State of ZK 2025 report (https://zkmesh.substack.com/subscribe) ----------- In this episode, Nico Mohnblatt speaks with Alex Hicks from the Ethereum Foundation about formal verification and its role in the lean Ethereum vision. This is the 6th and final episode of the lean Ethereum mini-series. Nico and Alex explore what it means to produce machine-checked proofs across the ZK stack, from RISC-V and zkVMs to circuits, compilers, and cryptographic primitives, and how these pieces connect in practice. The conversation also covers Alex’s path from physics and math into the ZK space, how the EF effort took shape, and the community push to formally verify the entire stack using proof assistants like Lean. They discuss efforts to formalize zkVM components, the tradeoffs between proof assistants and automated solvers, and what real progress looks like after a year and a half of focused work. Related Links * zkSummit14 applications are open! (www.zksummit.com) * lean Ethereum Part 1: Introduction with Justin Drake (https://zeroknowledge.fm/podcast/391/) * lean Ethereum Part 2: PQ Signatures and Poseidon with Dmitry and Benedikt (https://zeroknowledge.fm/podcast/392/) * lean Ethereum Part 3: Security of PQ SNARKs and an update about the Proximity Prize (https://zeroknowledge.fm/podcast/393/) * lean Ethereum Part 4: leanVM, a Custom VM for Signature Aggregation (https://zeroknowledge.fm/podcast/394/) * lean Ethereum Part 5: Devnets & Upgrade Coordination with Will and Raúl (https://zeroknowledge.fm/podcast/395/) * lean Ethereum (https://blog.ethereum.org/2025/07/31/lean-ethereum) * Lean Proof Assistant (https://lean-lang.org/) * Isabelle Proof Assistant (https://isabelle.in.tum.de/) * Lean Consensus R&D Progress (https://leanroadmap.org/) * Ethereum Foundation (https://ethereum.foundation/) ----------- **If you like what we do:** * Find all our links here! @ZeroKnowledge | Linktree (https://linktr.ee/zeroknowledge) * Subscribe to our podcast newsletter (https://zeroknowledge.substack.com) * Follow us on Twitter @zeroknowledgefm (https://twitter.com/zeroknowledgefm) * Join us on Telegram (https://t.me/+taXrPJIp_30zZTNi) * Catch us on YouTube (http://www.youtube.com/channel/UCYWsYz5cKw4wZ9Mpe4kuM_g) **Support the show:** * Patreon (https://www.patreon.com/zeroknowledge) * ETH - Donation address (https://etherscan.io/address/0xE2C080047213C1d8cDf2099E0B07479C5D9cee8a) * BTC - Donation address (https://www.blockchain.com/explorer/addresses/btc/bc1q9mrh34n6mvses59r3hq9dz6j3vxm3tlwlg8ws2) * SOL - Donation address (https://explorer.solana.com/address/Eqfm4maSDUN3ikjDfSgDeJ1mh3iC8tr69eHB5iTHz35x) * ZEC - Donation address (https://mainnet.zcashexplorer.app/address/t1gmdc8jKj4EXfYnNvwkToZUahx78GrQ2zv) 09:16 – What is formal verification? Proof assistants vs SMT solvers 18:33 – Formal verification of code: specs, semantics, and trust boundaries 29:30 – Formally verifying the Lean Ethereum stack: RISC-V ZKVMs in focus 33:02 – Extracting ZKVM constraints into Lean and proving soundness 36:35 – Writing constraints directly in Lean: 10–100x better proof ergonomics 44:02 – Proving Polishchuk–Spielman in 8 hours for $200 with AI 51:01 – The end goal: a full Lean stack bypassing Rust and LLVM