Zero Knowledge

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

Raúl Kripalani, Ethereum Foundation networking lead focused on transport and broadcast layers. Will Corcoran, research coordinator orchestrating DevNets and spec integration. They discuss DevNet progression and cross-team coordination. They dig into post-quantum signature impacts, bandwidth limits and EIP-7870. They explore next-gen ETH P2P design, erasure-coded broadcasts, subnetting, and prioritizing EL vs CL traffic.

Thomas Coratger, researcher and post-quantum team lead at the Ethereum Foundation, discusses LeanVM, a minimal zkVM built for signature aggregation. They explain why a VM was chosen over fixed circuits, the tiny 4-opcode design inspired by Cairo, and implementation choices like Plonky3 and WHIR for CPU-friendly proving. Benchmarks, recursion tradeoffs, and how the project invites community contributions are also covered.

Antonio Sanso, cryptography researcher at the Ethereum Foundation, and Giacomo Fenzi, EPFL PhD in coding theory, discuss post-quantum SNARK security. They cover hash-based proof systems, LeanVM’s multilinear sumcheck design, and the $1M Proximity Prize spurring work on proximity gaps, correlated agreement, and list-decoding. They also talk about recent papers shifting some guarantees from conjectural to computational security.

Benedikt Wagner, a PhD and cryptography researcher at the Ethereum Foundation focused on post-quantum signatures and Merkle constructions. Dmitry Khovratovich, a symmetric-crypto researcher at the Ethereum Foundation who works on Poseidon and hash-based designs. They discuss leanSig as a post-quantum BLS replacement. Topics include one-time signatures with Merkle trees, size versus verification tradeoffs, SNARK-based aggregation, hypercube encodings, and Poseidon’s role.

Justin Drake, Ethereum Foundation researcher focused on protocol design and post‑quantum readiness. He unveils Lean Ethereum and LeanVM, explaining how zk aggregation, hash-based post‑quantum signatures, and recursive SNARKs could shrink signature bloat. Short takes cover LeanVM’s ultra‑minimal ISA, enshrined vs off‑chain ZK proofs, formal verification efforts, and Poseidon2 as a snark‑friendly hash candidate.

A six-part video miniseries kickoff exploring lean Ethereum and its focus on weaving zero-knowledge cryptography and post-quantum upgrades into the stack. Topics previewed include hash-based signatures, formal verification, proximity gaps, and Poseidon hash work. They also explain the new video-first format and share details about an upcoming zk summit and how to get involved.

A short bonus segment revisits a deeper conversation about privacy trends and the changing narrative around Zcash. The discussion highlights research on limiting nullifier state growth without standard pruning. The show also previews subscriber-only perks and teases a six-part Lean Ethereum miniseries coming next week.

Ian Miers, Assistant Professor of Computer Science and ZK researcher behind zk-creds and zk-promises, explains stateful zero-knowledge identity primitives. He discusses anonymous moderation, reputation systems that avoid de-anonymization, ZK Cookies for continuous anonymous auth, and building self-sovereign, mutable pseudonyms for private group chats and moderation.

A short bonus clip explores whether quantum computers pose real threats to blockchains and Zcash upgrades. The conversation highlights technical perspectives on cryptographic risk and future-proofing systems. Listeners hear about subscriber-only perks and how to access extra members-only content.