lean Ethereum Part 6: Formal Verification with Alex Hicks

About this episode

Nico Mohnblatt speaks with Alex Hicks about formal verification and its role in the lean Ethereum vision.

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 Drake lean Ethereum Part 2: PQ Signatures and Poseidon with Dmitry and Benedikt lean Ethereum Part 3: Security of PQ SNARKs and an update about the Proximity Prize lean Ethereum Part 4: leanVM, a Custom VM for Signature Aggregation lean Ethereum Part 5: Devnets & Upgrade…

People in this episode

Host: Nico Mohnblatt

Guest: Alex Hicks

Topics covered

• formal verification
• lean Ethereum
• ZK stack
• machine-checked proofs
• cryptographic primitives
• proof assistants

Keywords

• formal verification
• lean Ethereum
• ZK stack
• machine-checked proofs
• proof assistants
• Ethereum Foundation
• zkVM

Mentioned in this episode

Organizations: Ethereum Foundation

Books & works: lean Ethereum

Places: Rome, Italy

More episodes of Zero Knowledge

• Building ZK-Powered AI Guardrails with Wyatt Benno · June 10, 2026 · 1h 7m
• The Quantum Question Panel – Live from zkSummit14 · May 27, 2026 · 59 min
• From Access Control to Encrypted Execution with Auryn Macmillan · May 20, 2026 · 53 min
• Quantum Advances, Hybrid Signatures and SNARKs to the Rescue with Dan Boneh · May 6, 2026 · 1h 25m
• Is ZK dead? Or has it just begun? with the ZK Pod co-hosts · April 22, 2026 · 1h 3m
• Verifiable Databases with Shyam & Emanuele from Provably · April 8, 2026 · 56 min