https://youtu.be/9u4fu7TiZCA
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
lean Ethereum Part 1: Introduction with Justin Drakelean Ethereum Part 2: PQ Signatures and Poseidon with Dmitry and Benediktlean Ethereum Part 3: Security of PQ SNARKs and an update about the Proximity Prizelean Ethereum Part 4: leanVM, a Custom VM for Signature Aggregationlean Ethereum Part 5: Devnets & Upgrade Coordination with Will and Raúllean EthereumLean Consensus R&D ProgressLean Proof AssistantIsabelle Proof AssistantEthereum Foundation
Applications to attend the zkSummit14 on May 7 in Rome, Italy are open! This edition will be more intimate with limited spots — we recommend applying early at www.zksummit.com
zkMesh+ live! Subscribe for zkMesh+ and catch the latest State of ZK 2025 report.
**If you like what we do:**
* Find all our links here! @ZeroKnowledge | Linktree
* Subscribe to our podcast newsletter
* Follow us on Twitter @zeroknowledgefm
* Join us on Telegram
* Catch us on YouTube
**Support the show:**
* Patreon
* ETH - Donation address
* BTC - Donation address
* SOL - Donation address
* ZEC - Donation address
Read transcript
