Four of us were on the latest Zero Knowledge podcast! 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, our framework for formally verifying circuits in Lean, and zk.golf, our competition to make those circuits cheaper. Here are a few excerpts.
From puzzles to circuit golf
Both Mathias and Giorgio met David through hiring challenges, without initially looking for a job. Kobi explains what made these puzzles useful in the first place (9:52):
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):
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.
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):
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):
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 points to a tutorial that assumes no prior experience with Lean or formal verification.
As Giorgio points out at 25:47: "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, and where circuit development and auditing might go next. Nico suggests a different kind of challenge (1:06:37):
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):
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 to pick a challenge!