{"podcast":{"title":"Zero Knowledge","slug":"zero-knowledge-1048106","podcast_index_feed_id":1048106,"rss_url":"https://feeds.captivate.fm/zeroknowledge/","website_url":"https://www.zeroknowledge.fm","image_url":"https://artwork.captivate.fm/eed81918-5c2c-4ed4-9ddc-11dbb519e2dd/cover.jpg","author":"Zero Knowledge Podcast","episode_count":420,"summary":"Zero Knowledge is a podcast which goes deep into the tech that will power the emerging decentralised web and the community building this. Covering the latest in zero knowledge research and applications, the open web as well as future technologies and paradigms that promise to change the way we interact — and transact — with one another online. Zero Knowledge is hosted by Anna Rose Follow the show at @ZeroKnowledgefm (https://twitter.com/zeroknowledgefm) or @AnnaRRose (https://twitter.com/AnnaRRose) If you like the Zero Knowledge Podcast: Join us on Telegram (https://t.me/joinchat/TORo7aknkYNLHmCM) Support our Gitcoin Grant (https://gitcoin.co/grants/38/zero-knowledge-podcast) Support us on Patreon (https://www.patreon.com/zeroknowledge) Or directly here: ETH: 0x4BF66E52f3009Cd138e48f142D47661037160001 BTC: 1cafekGa3podM4fBxPSQc6RCEXQNTK8Zz ZEC: t1R2bujRF3Hzte9ALHpMJvY8t5kb9ut9SpQ DOT: 14zPzb7ihiBeaUn9jdPW9cHKGBd9qtTuJE75hhW2CvzLh6rT","last_synced_at":"2026-07-30T02:18:37.841188+00:00","page_url":"https://stenobird.com/podcast/zero-knowledge-1048106"},"episode":{"title":"lean Ethereum Part 6: Formal Verification with Alex Hicks","slug":"lean-ethereum-part-6-formal-verification-with-alex-hicks","published_at":"2026-03-25T13:00:00+00:00","page_url":"https://stenobird.com/podcast/zero-knowledge-1048106/lean-ethereum-part-6-formal-verification-with-alex-hicks","show_page_url":"https://stenobird.com/podcast/zero-knowledge-1048106","url":"https://zeroknowledge.fm/podcast/396","audio_url":"https://episodes.captivate.fm/episode/a92b7710-a3d3-40ba-81dc-f5fce1f6b970.mp3","summary":"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 u…","meta_description":"https://youtu.be/9u4fu7TiZCA In this episode, Nico Mohnblatt speaks with Alex Hicks from the Ethereum Foundation about formal verification and its role in…","key_points":[],"chapters":[],"topics":[],"duration_seconds":3462,"processing_state":"not_requested","actions":[{"name":"request_transcript","method":"POST","url":"https://stenobird.com/v1/public/podcasts/zero-knowledge-1048106/episodes/lean-ethereum-part-6-formal-verification-with-alex-hicks/transcription-requests","description":"Idempotently request low-priority transcript generation for this episode."},{"name":"read_markdown","method":"GET","url":"https://stenobird.com/podcast/zero-knowledge-1048106/lean-ethereum-part-6-formal-verification-with-alex-hicks.md","description":"Read the agent-friendly Markdown representation of this episode resource."}]}}