zkGolf: AI, Clean and Optimising ZK Circuits with zkSecurity

This week, Anna is joined by Nico and Kobi to speak with Mathias Hall-Andersen and Giorgio Dell'Immagine from zkSecurity about zkGolf, a competition challenging humans and AI agents to build the most efficient, formally verified ZK circuits. They look back at ZK Hack puzzles and CTFs, exploring how AI is changing the nature of technical competitions. They then dive into Clean, zkSecurity's framework for writing and formally verifying circuits in Lean, and how an experiment using AI to optimize a SHA-256 circuit inspired zkGolf. They discuss how the zkGolf competition works, the breakthroughs and exploits participants have uncovered, how it compares to other AI-driven optimisation challenges, and what AI-assisted circuit development could mean for the future of ZK engineering and security audits.   Related Links  

• zkGolf Website
• Clean GitHub Repo
• Clean Website
• Lean Programming Website
• ZK Hack
• Yukon Website
• ZK Podcast: Auto Research on Yukon with Soubhik Deb
• ZK Podcast: Alex Ozdemir on where Theorem Provers and ZK meet
• ECDSA.fail
• SNARK.fast Flock Challenge
• The Proximity Prize

    Sovright builds the critical infrastructure that preserves your right to choose. Discover more at sovright.com.     **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 Read transcript