# Zero Knowledge Episode 414: zkGolf, AI, Clean and Optimising ZK Circuits - **Authors**: ZK/SEC - **Date**: October 21, 2026 - **Tags**: announcement, zk, clean, formal-verification, ai Four of us were on the latest [Zero Knowledge podcast](https://www.youtube.com/watch?v=h91njed8__s)! Mathias Hall-Andersen and Giorgio Dell'Immagine joined Anna Rose and co-hosts Nico Mohnblatt and Kobi Gurkan for **Episode 414: zkGolf: AI, Clean and Optimising ZK Circuits with zkSecurity**. The conversation follows the path from cryptography puzzles to [Clean](https://clean.zksecurity.xyz/), our framework for formally verifying circuits in Lean, and [zk.golf](https://zk.golf/), our competition to make those circuits cheaper. Here are a few excerpts. https://www.youtube.com/watch?v=h91njed8__s ## From puzzles to circuit golf Kobi explains what made cryptography puzzles useful in the first place ([9:52](https://www.youtube.com/watch?v=h91njed8__s&t=592s)): > One thing that I found useful, both for myself and people around me, is that one of the best ways to learn something deeply is to try to break it and to see what goes wrong and what needs to be done for it to go right. With agents now solving the puzzles, what should the next competition look like? Nico sums up zkGolf ([39:53](https://www.youtube.com/watch?v=h91njed8__s&t=2393s)): > Yeah, it's write an R1CS circuit that matches my spec and that has low cost and prove that you match my spec and have low cost. We tell the story of the first experiments in [our zkGolf launch post](https://blog.zksecurity.xyz/posts/zkgolf/). ## Let the agent write the circuit, and ask for a proof Giorgio describes the question behind Clean and the experiments that led to zkGolf ([19:35](https://www.youtube.com/watch?v=h91njed8__s&t=1175s)): > And the main point is that, how do you ensure that what the LLM has written is actually what you wanted? And so we were kind of discussing of this idea that maybe if the LLMs can prove that what it wrote was what you wanted, then you could trust the implementation. The same approach applies to the score. Mathias, on requiring proofs of the circuit's cost as well as its correctness ([33:58](https://www.youtube.com/watch?v=h91njed8__s&t=2038s)): > I'm asking it to grade its own homework, but I'm going to verify that it graded correctly. It's going to prove that it graded correctly. If you'd like to try it, our [introduction to Clean for developers](https://blog.zksecurity.xyz/posts/clean-for-programmers/) points to a tutorial that assumes no prior experience with Lean or formal verification. > [!NOTE] The specification still matters > > As Giorgio points out at [25:47](https://www.youtube.com/watch?v=h91njed8__s&t=1547s): "Clean gives you a way to check and to prove that your circuit and specification are equivalent. There could be also bugs in the specification." ## Understanding what the agents discover The episode also covers bugs found in the competition's definitions, the connection to [Better.Codes](https://blog.zksecurity.xyz/posts/better-codes/), and where circuit development and auditing might go next. Nico suggests a different kind of challenge ([1:06:37](https://www.youtube.com/watch?v=h91njed8__s&t=3997s)): > We could start to do the same with zkGolf or we could have sort of a reverse hackathon so I don't want you to go and create something I want you to go and explain something that's been created And for anyone wondering whether it's too late to compete, Mathias says ([1:10:39](https://www.youtube.com/watch?v=h91njed8__s&t=4239s)): > Just when we thought we'd hit rock bottom apparently the bottom fell out and we're taking suggestions for circuits as well Watch the full episode above, or head to [zk.golf](https://zk.golf/) to pick a challenge! --- This article was published on the [ZK/SEC Quarterly](https://blog.zksecurity.xyz) blog by [ZK Security](https://www.zksecurity.xyz), a leading security firm specialized in zero-knowledge proofs, MPC, FHE, and advanced cryptography. ZK Security has audited some of the most critical ZK systems in production, discovered vulnerabilities in major protocols including Aleo, Solana, and Halo2, and built open-source tools like [Clean](https://github.com/Verified-zkEVM/clean) for formally verified ZK circuits. For more articles, see the [full list of posts](https://blog.zksecurity.xyz/llms.txt).