About this episode
This week, Anna and Nico are joined by Alex Ozdemir, Assistant Professor at Georgia Tech, to explore the intersection of formal verification and zero knowledge. They begin by revisiting the evolution of the ZK DSL landscape since Alex's last appearance, discussing the rise of ZKVMs, new language tooling, and how his compiler infrastructure project, CirC, has evolved.
The conversation then dives into formal verification and theorem proving, covering SMT solvers, Lean, and zkPi, the first zkSNARK for proofs expressed in Lean. They also discuss compiler correctness, the challenges of verifying cryptographic systems, and why verifiable software will become increasingly important as the industry matures.
Related Links
ZK Podcast and Alex Ozdemir
**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
- zkPi: Proving Lean Theorems in Zero-Knowledge
- CirC: Compiler infrastructure for proof systems, software verification, and more
- Kevin Lacker on AI-Assisted Theorem Proving and Acorn
- Building ZK-Powered AI Guardrails with Wyatt Benno
- lean Ethereum Part 6: Formal Verification with Alex Hicks
- Groth16, IVC and Formal Verification with Nexus
- lean Ethereum
ZK Podcast and Alex Ozdemir
- ZK languages with Alex Ozdemir
- zkSessions: Alex Ozdemir - The Taxonomy of Circuit Languages
- zkStudyClub: Collaborative zkSNARKs (Alex Ozdemir, Stanford University)
- zkStudyClub: Unifying Compiler Infrastructure for SNARKs, SMTs, & More w/ Alex Ozdemir (Stanford)
- ZK HACK - Introduction to Domain Specific Languages (DSLs) - Alex Ozdemir
**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
Get every episode summarized
Each time Zero Knowledge publishes, we email you a written briefing from the transcript — the topics, who appeared, and any specific claims, with the ad reads skipped.
Email me new episodesFree for 3 shows. No card needed.
Hosts & guests
No transcript yet
This episode has not been transcribed. Request it and it moves to the front of the queue.
More episodes
More from Zero Knowledge
The Evolution from ZKP2P to Peer with Richard Liang
Zero Knowledge
Sep 9, 202646:00completed
Minimmit, Multimmit and the New Consensus Frontier with Patrick O'Grady
Zero Knowledge
Aug 5, 20261:12:01pending
Private Information Retrieval (PIR) with Alex Hoover
Zero Knowledge
Jul 29, 20261:04:13pending
Sergey Gorbunov on TEEs and the Arc Privacy Sector
Zero Knowledge
Jul 8, 20261:07:07pending