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 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 Coordination with Will and Raúl
lean Ethereum
Lean Consensus R&D Progress
Lean Proof Assistant
Isabelle Proof Assistant
Ethereum 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

https://youtu.be/Ul2bs8INF0k

In this episode Nico Mohnblatt chats with Will Corcoran and Raúl Kripalani from the Ethereum Foundation. This is part 5 in the 6-part leanEthereum miniseries, shifting focus from the cryptographic primitives and LeanVM stack to the real-world integration happening through devnets, specs, and cross-team coordination.

They dive into the human coordination layer, how independent teams align on post-quantum signatures, SNARK aggregation, and protocol changes, plus the networking upgrades needed for larger payloads.

Raúl explains the shift from today's libp2p stack to a purpose-built Eth P2P next-gen version optimised for Ethereum's workloads, including better broadcast layers, erasure coding, and control planes to handle bandwidth competition between execution and consensus layers.
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
Lean Consensus R&D Progress
Ethereum 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

https://youtu.be/YWkyvTrwtQU


In this episode of the lean Ethereum miniseries, Nico Mohnblatt speaks with Thomas Coratger and Emile from the Ethereum Foundation about the design and implementation of LeanVM, a minimal zkVM created to support post-quantum signature aggregation on Ethereum’s consensus layer. They explain why the team chose a VM architecture over fixed circuits and how LeanVM takes inspiration from Cairo with just 4 opcodes and 2 precompiles to keep the instruction set extremely small and make formal verification easier.

The conversation also covers LeanVM implementation choices like using Plonky3 and WHIR for efficient proving on CPUs, benchmarks for aggregation speed, and the role of Python specs in testing client interop. They share ongoing efforts to optimize low-level primitives and invite community input on the project.


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
Lean Consensus R&D Progress
Cairo zkVM
WHIR: Reed–Solomon Proximity Testing with Super-Fast Verification
Minimal zkVM for Lean Ethereum by Emile


Repos

leanEthereum github organization
leanSig repo (optimized Rust implementation of XMSS for Ethereum usage)
leanSpec repo (the Python spec of the lean consensus)
WHIR repo
Plonky3 repo
leanVM








Applications to speak at zkSummit14 close this Sunday March 15! This edition will be more intimate with limited spots — we recommend applying early. Apply 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

https://youtu.be/v8SGKS3T-3A

In this episode, Nico Mohnblatt speaks with Giacomo Fenzi from EPFL and Antonio Sanso from the Ethereum Foundation. For this 3rd instalment of the lean Ethereum miniseries, they talk about the theory and security behind post-quantum SNARKs. They dive into the hash-based proof systems underpinning LeanVM, multilinear approaches like sumcheck, and how these fit into Ethereum's post-quantum upgrades.

They cover the $1M Proximity Prize and the recent wave of papers on proximity gaps, correlated agreement, and list decoding. From negative results near the Elias bound to breakthroughs beyond the Johnson bound for certain codes, the discussion explores how new results slightly degrade conjectural security, why the 128-bit threshold still matters, and what it means to move from conjectural to provable security in large-scale systems like Ethereum.
Related Links

lean Ethereum Part 1: Introduction with Justin Drake
lean Ethereum Part 2: PQ Signatures and Poseidon with Dmitry and Benedikt
lean Ethereum
Lean Consensus R&D Progress
leanSig Implementation
Poseidon2: A Faster Version of the Poseidon Hash Function
On Proximity Gaps for Reed–Solomon Codes
Proximity Gaps in Interleaved Codes
On Reed–Solomon Proximity Gaps Conjectures
Optimal Proximity Gaps for Subspace-Design Codes and (Random) Reed-Solomon Codes
All Polynomial Generators Preserve Distance with Mutual Correlated Agreement


Additional Resources

Soundcalc GitHub
Proximity prize
On the Distribution of the Distances of Random Words
Small-field hash-based SNARGs are less sound than conjectured by Fenzi and Sanso
WHIR: Reed–Solomon Proximity Testing with Super-Fast Verification
STIR: Reed–Solomon Proximity Testing with Fewer Queries
Linear-Time Accumulation Schemes
TensorSwitch








Applications to speak at zkSummit14 are now open! This edition will be more intimate with limited spots — we recommend applying early. Apply 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

https://www.youtube.com/watch?v=xh8hbz1nqxQ

In this episode, Nico Mohnblatt speaks with Benedikt Wagner and Dmitry Khovratovich, cryptography researchers at the Ethereum Foundation, for the second instalment of the lean Ethereum miniseries. They explore leanSig, a hash-based multi-signature scheme designed as a post-quantum replacement for BLS in Ethereum consensus.

The conversation walks through how one-time signatures and Merkle trees can be combined to support long-lived validators, and why SNARK-based aggregation is needed in a post-quantum setting. The talk touches on key tradeoffs like signature size versus verification speed, encoding challenges behind their At the Top of the Hypercube work, and the role of Poseidon as the core hash function.
Related Links

lean Ethereum Part 1: Introduction with Justin Drake
lean Ethereum
Lean Consensus R&D Progress
leanSig Implementation
Poseidon2: A Faster Version of the Poseidon Hash Function
At the Top of the Hypercube – Better Size-Time Tradeoffs for Hash-Based Signatures
Hash-Based Multi-Signatures for Post-Quantum Ethereum
Technical Note: LeanSig for Post-Quantum Ethereum
Aborting Random Oracles: How to Build them, How to Use them
The Billion Dollar Merkle Tree 
Poseidon: A New Hash Function for Zero-Knowledge Proof Systems
Poseidon Cryptanalysis Initiative








Applications to speak at zkSummit14 are now open! This edition will be more intimate with limited spots — we recommend applying early. Apply 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