zkGolf: AI, Clean and Optimising ZK Circuits

Transcript

Welcome to Zero Knowledge. I'm your host, Anna Rose. In this podcast, [music] we will be exploring the latest in zero knowledge research and the decentralized web, as well as new paradigms that promise to [music] change the way we interact and transact online. This week, Nico Koby and I speak with Matthias and Giorgio from ZK Security. The through line of the episode was the topic of ZK Golf, a competition set up by ZK Security that challenges people and their agents to build the most efficient circuits possible formally verified in Lean.

We start with a bit of history, looking back at the ZK hack puzzles and how CTFs and challenges like these have long been a way for people to learn, get recognized, and potentially get hired. But, with AI tools being as powerful as they are, these competitions basically been made obsolete. And so, we need new types of competitions like ZK Golf. From there, we dig into Clean, ZK Security's framework for writing ZK circuits in Lean and formally proving that they match a specification. Matthias and Giorgio share how an experiment where they asked an AI to write and prove a circuit, then put it through a loop to drive down its cost, ended up producing the best SHA-256 circuit they'd ever seen.

That experiment evolved into ZK Golf, an open competition where anyone can submit a circuit as long as they can prove it's correct and prove how efficient it is. We talk about how ZK Golf compares to the Yukon competition we covered recently on the show, and what this could mean for how circuits get written and audited in the future. So, hope you enjoy. Now, Tonya will share a little bit about this week's sponsor. Today's episode is sponsored by Sovryn. Sovryn builds the critical infrastructure that preserves your right to choose. Sovryth has built two products, Argos and the Sovryth mining pool.

Argos is a free tool that lets anyone with ZEC stranded in an old unmaintained wallet client recover their funds. Enter your seed phrase, generate a new address, and your money is yours again. No fees, no complexity. The Sovryth mining pool is Zcash native and built on Stratum V2, where miners choose their own transactions. Every block carries a verifiable signed attestation and payouts arrive in fully shielded ZEC. Two essential problems that have been overlooked finally solved. Discover more at sovryth.com.

So, thanks again, Sovryth. And now, here's our episode. Today, I'm here with Nico, Kobe, and two of their colleagues from ZK Security, Giorgio and Matthias. Hi, Nico. Hi, Kobe. >> Hello, everyone. >> Hello. >> [laughter] >> Hi, Giorgio. Hi, Matthias. >> Hello, everyone. >> Hello. >> All right. So, I want with this episode to explore the topic of ZK Golf. I recently did an episode on Yukon on the platform where they're running a lot of these competitions.

I feel like ZK Golf fits sort of in that category, but I haven't quite understood the distinction between these two initiatives. So, I'm hoping we get to dive into that with this episode. But, maybe before we do that, Giorgio, Matthias, you are new to our audience. So, why don't we find out a little bit about you? Matthias, can you start? Share with us a little bit of your origin story and yeah, how ZK Security came about. >> Yeah, so I'm one of the co-founders of ZK Security and I have a PhD in cryptography and work on cryptography at ZK Security, not surprisingly.

Originally, I I met David back in NCC Group. I worked together doing audits as back in like 2018. And then he he went and joined first Meta and then and then Mina. >> Mhm. >> And while he was busy doing that, I was busy doing PhD. And then eventually when I was wrapping up my PhD, we did some audits together. And he suggested that I that I come on board and and do this thing together with him and and Gregor and Brandon at the time. >> Cool. In your PhD work, were you touching ZK stuff? Like what kind of cryptography were you working on?

>> Yeah, it's it's almost exclusively ZK and and and MPC. >> Okay. What did you like about those paradigms? >> I've always been amazed at cryptography because it it seems like like magic, frankly. Like you do things that seem very counterintuitive to the average person that perhaps the even even somebody with a computer science degree could argue is impossible. >> Mhm. >> And I think ZK is a is is probably the best example of this, especially to sync proofs. I'm I'm very interested in there. Essentially magic to to the outside observer, it's it's it's actually surprising that this is even even possible.

>> Mhm. So, you did ZK and MPC. Do you feel like MPC has also developed as much as ZK? Or do you feel like it's a different I don't know. Like it does it seem to be going at a different pace? I'm curious if you're really observing both of those, what you make of the distinction. >> First and foremost, there's a rich connection between the two, right? Obviously, you can use zero-knowledge proofs in MPC protocols for instance to make them maliciously secure. And there's also something called the Icos compiler that takes any any MPC protocol and turns it into zero-knowledge proof.

>> Okay. >> Uh which has been used for for instance built post-quantum signatures. So, there is there's a there's a big connection. In terms of applications, I MPC sort of hasn't taken off in the same way in practical applications. I think the only the only sort of real deployments of MPC are really key management. >> Mhm. Why is that? Is it just like that is the use case where it best fits? Or has there not been as much like mind share focused on it? Is it because it didn't blend as well with blockchain or something? >> It's still relatively slower.

>> Okay. >> And it's also often times hard to find parties to compute with. I think it's actually the the biggest issue for MPC. In addition to being slow, it's like what what are you trying to compute? And and and who what are you trying to compute this this with? >> Mhm. >> The the setting for MPC like sort of relatively rarely comes up. And I think the more practical version of MPC in a lot of cases turns out to be fully homomorphic encryption with like threshold encryption. And very concretely, MPC requires interaction, right? Whereas ZK, we have our nice non-interactive proofs. I send you my proof and I move on with my life and you do whatever you want.

>> I guess there is no way to make an MPC non-interactive because you need this like multi-party is in the name. >> Technically, there is something called like non-interactive MPC, but obviously the it's subject to something called a residue problem. It's actually so you you send something to one party and they can sort of compute the result. But obviously, they can compute any additional like they can they can change their own input and compute whatever other function they want. >> Mhm. >> So it's it's it's a very limited what you can do. >> Got it. Okay, so you joined ZK security with David. You co-founded that. Has that been a big shift to like go cuz you're kind of back in in industry now away from academia. What's that shift been like?

>> It doesn't feel that much like like industry. >> No. >> Right. Like I'm not I'm not I'm not looking at I'm not looking at at TLS implementations, right? Like yeah. >> [gasps] >> I I I have the fortune to Basically, like a large fraction of our of our customers are extremely intelligent people who have defined extremely complicated systems for for me to take a look at. So it doesn't really feel that much like industry. It's the It's the softest possible landing. >> Oh, nice. >> [laughter] >> Cool. All right, Georgio. Let's learn a little bit about your background and what you do at ZK Security.

>> Sure. So, I became interested in cryptography I will say three or four years ago. >> Mhm. >> I was doing CTFs at the time. I was also doing my masters. And then there was this, you know, one of the categories of CTFs usually is cryptography. And then at some point I I don't know when exactly, but at some point I decided, "Okay, maybe I I can take this seriously." And then I started like studying a lot. >> Cool. >> And I met ZK Security because they had a challenge like a hiring challenge, but I didn't know it was a hiring challenge.

>> Oh, you just thought it was a puzzle? >> it for the Yes. So, I did it just for [laughter] the fun. But then, okay, I messaged David. And then he was like, "Oh, are you free?" >> [laughter] >> And then and then, you know, I joined. >> I love this accidental hiring situation. >> Yeah. >> [laughter] >> It's actually not too dissimilar to how I I I met David originally. So, he had a blog. This is back in like 2016 or something. >> Oh, yeah. >> And he posted like a challenge a hiring challenge for NCC Group. And I solved it and I was like, "But I'm not interested in >> [laughter] >> in a job. I just like want to flex that I solved this thing."

>> [laughter] >> Nice. >> Yeah, and that that continues the the line that we see I guess in this industry where puzzles lead to amazing hires. >> Totally. And I mean this in a way leads us to what we're going to be talking about, which is ZK Golf. I want to mention something that Kobi and I were doing back in 2021 all the way to 2024 25, which was the ZK Hack online competitions. And the reason I want to mention that is basically your story Giorgio and what you described Matias about finding your way into an ecosystem or into a company through participating in what is maybe seems more like a fun challenge at the

beginning. Back in 2021 Kobi had this idea for these ZK hack puzzles. Kobe, do you want to just I mean, I think most of the audience is familiar with it. I tend to work it into all conversations lately around [laughter] auto research, but maybe you want to just define what the initial idea was and kind of what we did with it. >> Uh yeah, so the initial idea first I thought it would be fun because there weren't so much puzzles around advanced cryptography I've been seeing around me, especially around snarks, ZK, and this kind of protocols that we touch in in this part of this industry.

And 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 what goes wrong and what needs to be done for it to go right. And that was one of the main reasons that I thought ZK hack puzzles would be useful. So it ended up being a really nice tool for people to learn about these protocols. And initially we tried to take puzzles of protocols and problems that we've seen.

So actual protocols, things that would have an impact in real life if they were to break in that way. >> Mhm. >> Which is sometimes different than what you would see in an academic course, which seems a bit artificial. And I I think also the ZK ZK security challenges are of that form. >> Mhm. >> Which is nice. And yeah, I think one of the things that we've seen when we run the puzzles is that it got a few new people into the field that they were trying to find a way to kind of have a foot in the door.

And they became experts and top people in the field, which was which is great. And also I guess well, personally or team-wise it was nice for me because I managed to hire people that I've seen there. So, for example, I mean in geometry research, that that was one way that we found good people. >> Yeah, ZK Hack one is how I got in. >> So, cool. >> Yeah. >> I sort of wanted to throw ZK Hack out there because that was for me at least, that was the first time that I saw that phenomenon of like you put up challenges, they're just for fun, and then people break them, and then you can see those people enter into the ecosystem, maybe get hired. You start working with them, or you know, we have

some folks who participated in that first one, and then ended up presenting at like the third one or something. Like they started to become the educators for the next batch. But, I also kind of mentioned this Kobe a little bit as like a like I feel like the ZK Hack online puzzles as they existed no longer work because and I think even the last edition we did, we started to see that because LLMs were really coming online and being capable, it was harder to tell what a person was doing versus an AI.

>> Yeah. I I think that's true. I don't remember exactly, but I do remember that when we were reviewing the submissions part of the write-ups where so, we had the puzzles where people have to solve problems, but we also had the write-ups where people would write about what was the issue, what was the solution, and what was the problem, and so on. And I think there we've started seeing that people were using AI more heavily to write about it, and sometimes it didn't make a lot of sense.

Sometimes it did. Um we still, you know, our goal was to choose the best one, so that's okay. That was still our job to curate it. But, yeah, we started seeing that, and I think since the last one we've ran, we've seen this big explosion of how productive these tools can be both in productive work, but also in exploit world. >> Mhm. >> And that is exactly what the key puzzles look like. So, probably it would be much much harder to design puzzles >> today.

>> in that same form, yes. >> Giorgio, you mentioned you were doing a lot of CTFs. I actually wonder the CTFs that you used to participate in, are those still around? >> Well, they are still around, but there's basically nobody playing them anymore. >> Oh, really? >> Because it doesn't really make sense. >> Wow. >> Yeah. It's kind of sad that CTF scene has been dying since I think 6 months. >> Yeah. >> Basically after GPT 5.5 came out, every challenge was solvable by just ask an agent to to solve it.

And so, even hard ones. >> Yeah. >> And so, that was kind of sad. >> What you can do these days for fun is bring up the ePrint queue and ask an agent break >> [laughter] >> break one of these papers. >> Yep. >> [gasps] >> That's the new CTFs. >> That's the new CTF. We had JP almost on the show recently and he was talking about how the NIST standards would come out and all the PhD students would try to break or the NIST candidates or whatever, they'd come out and then people would try to break them, but now that's sort of lost its fun, too, because they're getting broken too quickly.

Like if there's something to break, it will be broken quickly by an LLM and there's no time for the PhD student to spend time like digging through and figuring it out. >> And what what what puzzles me the most is that the authors submitted those candidates without, you know, feeding them to an LLM first. >> Yeah. My thinking on that, I mean, we we were talking about the Chinese standardization competition. My thinking was like why are they all getting broken? And maybe it's that they had to submit it a few months ago or something like that and the models have caught up. Like the models that they were testing it on weren't as you know effective as the ones that are available today.

Another kind of rest in peace moment for ZK Hack I want to mention on the show cuz we haven't really talked about this either is hackathons. I think we did in total five in person three-day hackathons around the ZK Hack concept right as ZK products and tooling were like they became usable and so people could now build with them and so we did these hackathons and the last one we did was in Berlin last year and it was a really kind of beautiful moment because LLMs were they had come online a little which meant that like the project submissions were beautiful but you could still identify what was like made by a human and made by an LLM. So you could also see if

something was just kind of fluffy or if it was like actually interesting. But I really wonder if there's a future for hackathons in the way that we've known them because I think judging hackathons will become I mean are already almost impossible to do. >> Mhm. >> I don't know if anyone here ever participated in hackathons. I know Nico you judged a couple. Kobe I think you judged one too, right? >> Yeah. >> Across the years. >> [laughter] >> I actually judged and participated in some of the ZK Hacks but I never went for like the the pretty projects like I would go for the chewing glass kind of thing that you have in ZK Hack where you implement nasty cryptographic primitives and the judges are impressed and reward you for it.

>> [laughter] >> But again I think today that's also over and we'll talk about this a bit more later I think but LLMs are good at implementing cryptography. >> For sure. I think this is a really good moment to switch over to ZK Golf. I think we've given a little bit of the history and yeah I want to understand what is ZK Golf, where does the idea for ZK Golf come from? Like, is it inspired by the puzzles of ZK Hack? Is it inspired by something else? Where did it start? >> Yeah, so it it started with this work which Georgia was more more involved in originally than than me.

Together with with Gregor. Where we we wrote a framework called clean for formally verifying circuits. So, essentially you can prove that your ZK circuit satisfies certain properties or is equivalent to some And we did this last year. So, every all the circuits were mostly written by humans and all the proofs were mostly written by humans because the LLMs were not very good at writing proofs at that point. And I think even last year we even tried to to get Claude like last spring spring 2025.

We tried to get Claude to write even basic proofs and he was spinning forever and didn't manage to apply reflexivity, I think. So, he didn't manage to prove that like A is equal to A basically. So, that experience it sort of left us to discount, you know, LLMs in this domain for for a while. But then around, I guess, March, I suggested to Georgia that, you know, he's he's writing a specification for a hash function called or the hash function SHA-256. And I suggested that, you know, maybe you should just try and ask an an LLM to to write the the circuit and and and ask it prove that that this circuit is is is secure.

And surprisingly this I guess surprisingly to Georgia at the time it it it succeeded. I I suggested this because I I've been playing a little bit with LLMs and and Lean at this time mostly because I was like learning Lean at the time and it's it's a great learning tool. Essentially, you can you can get it to to write things for you and explain things for you and then, you know, instead of having to climb this immense hurdle of like starting from nothing, you essentially have a have a tutor, right? And I was like very very impressed with that. So, I figured they they could probably we write these these proofs.

For context, these are not, you know, mind-blowing proofs of Navier-Stokes or anything, right? Like these are extremely banal proofs about like equivalences of like, you know, this is a byte and it's equivalent to like eight bits, right? Like these are like really, really banal proofs. So, yeah, and at that point it was sort of like right at the at the cusp where LLMs could could could write these proofs. >> We were discussing a lot of this like futuristic idea of letting LLMs write stuff for us. 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 LLM can prove that what it

wrote it was what you wanted, then you could trust the the implementation. And so, you could only focus on higher-level properties or like what you want or like, you know, some brain-computer interface like ideas. But yeah, it was this this idea that all the details, you know, you figure it out and I want to only talk about very abstract, very high-level objects. And this is kind of what we do with compilers, right? So, we have high-level languages and nobody looks at the assembly because the compiler takes care of all the details.

>> Mhm. >> And one trust assumption we have when we write in high-level languages is that the compiler is correct. While we are taking like the other approach, which is like let's also write the low-level language, but let's prove that it's equivalent to the to the high-level program or the specification, whatever you want to call it. Yeah, and so we were like, okay, let's just write a SHA-256 implementation in Lean and let's just ask an LLM to provide a circuit which is probably equivalent to this SHA-256 implementation.

But yeah, and it run I think for I don't know, four or five days. It was still in the moments where you had to baby sit kind of the the agent to to do its its stuff. So, you could say like, "Yeah, try this, try that." And And the first circuit was not good. It was all that the bit level. The gates were all the naive ones. But, you know, it worked. And so, we were like, "Okay, let's just push it to to the library of clean." >> But, this was just you internally running this, right? This was like an experiment. You hadn't like published this externally yet. You weren't talking about this with the community.

>> No, we I think I pushed the PR on clean. >> Okay. >> And so, the the circuit was there. But, yeah, we didn't really talk about it publicly. >> What is So, let's talk about clean. Clean, I guess. What is it Is it circuit lean? What is it? What's the C for? >> I honestly don't know. Or I don't remember. >> [laughter] >> What was the reason? Yeah, probably circuit lean. >> Matthias, do you know? >> Yeah, it's a it's circuit lean. >> Okay, that's okay. >> I think I think Gregor told me at one point that it's circuit lean. >> Okay.

>> Yeah, so clean is a framework to write circuits in lean. So, it's a mini DSL for representing circuits. So, the the way to think about lean in kind of from from first principles is that there are very beautiful theoretical results that link logic, so mathematics, and type theory. And so, whenever you write a program, you can actually show that every program is isomorphic to a proof, and every type is isomorphic to a proposition.

And the act of checking a proof to be a valid proof for some proposition is actually equivalent to the act of type checking. So, lean is in some sense both a programming language and a proof assistant, meaning that you can encode logic into types, but then you can also use types for the computation like a normal programming language. And so, it's it is this very beautiful idea that you can encode mathematical objects and propositions into types, and then the Lean kernel basically does type checking in a type system which is kind of crazy.

So, it's you know, it's not the usual type system we are used to, for example, Rust or in C. But, it turns out that this very complex, very very rich type systems can encode a lot of logic, a lot of propositions. >> And so, within that Clean is a way to express circuits as types? Like, can you explain a bit more how Clean fits into the picture? >> Yeah, so Clean is a way basically is a is a framework to write circuits. And what Clean does, it's basically provide what does it mean to write a circuit?

So, for example, in Clean you can say assert zero on some expression, and you know, Clean says, "Okay, this assertion enforces that this expression is equal to zero." >> Mhm. >> And so, you can write circuits, and then you can reason about them because you know what it means, for example, to enforce constraints. So, in Clean, for example, we have mainly two properties that we care about circuits. You can extend it to prove other properties, but the main two properties are soundness and completeness. And we always reason about circuits and what's called a specification.

So, a specification is nothing more than a program or a high-level program. >> Mhm. >> And improving soundness, you're proving that your circuits for every satisfiable assignment to the circuit, the same assignment pass the specification and in completeness you are proving that you can actually find a satisfiable assignment to your circuit. So, soundness basically rules out under constrained circuits and completeness rules out over constrained circuits. And so the combination of both let us uh the say that the circuit is probably equivalent to the specification in this kind of well we can make it more precise with

soundness and completeness but it can be abstracted away and said saying that this circuit implements this function and the function is given in the specification. >> Okay. >> Does that mean that Lean is inherently bug free? Like can I not introduce bugs by using Lean? >> Um >> Trick question by the way. >> Yes. [laughter] Um there's still a trusted base. >> Mhm. >> Well first of all, I mean the the obvious trust assumption that we are using is that Lean is correct. Like there are no kernel bugs and uh >> Oh.

>> in particular the kernel does not have the the logic of Lean is consistent and so you cannot prove false. But that's kind of uh we are not really interested in soundness bugs. We are more interested in you know if what we are actually enforcing with Lean is what we meant. So Lean gives you a way to check and to prove that your circuit and the specification are equivalent. >> Mhm. >> There could be also bugs in the specification. >> Yeah. >> So the specification is just another program. Right? And so for example, one of the the things for which it doesn't really make sense to formally verify software is if your specification is roughly the same complexity as your implementation.

Right? So if I just rewrite my program and the circuit was 100 lines and the specification is 100 lines and the logic is the same. Right? I'm just proving that you know those are equivalent but I'm not really taking advantage of this. >> Oh. >> Because I still need to review the specification, and so why don't I just review the circuit, right? If it's the same complexity. But one of the challenges we have in ZK Golf, and maybe we can talk about We haven't really talked about what is ZK Golf. Uh is RSA signature verification, and the specification is basically one line.

And the circuit is, I don't know, 10,000, 20,000 lines of code. And so, but you need only review that one line of code. Well, I have oversimplified. It's not one line. It's like 200, but >> Maybe before we dive into ZK Golf, though, just to further dig into clean, Kobi, in the context of what we described before with the puzzles, could you have ever used something like clean with those puzzles to find the issue, or would you have had to have a perfect system output a like, "Yes, this works." Like, would Does it actually identify what's wrong, or does it need everything to work for it to sort of say, "Yes, this is correct."

>> Yeah, that that's that's a very good detail to to go into. So, I think in the puzzles that we had, we had a few different kinds. I'm if I'm remembering correctly, we did have at least one that is about under constrained circuits. So, if the specification is written correctly, then clean would not would not say it's sound. >> It would just output false, or what is it like What is it >> It will not compile. >> It won't compile. Okay. >> You will not be able to create a soundless proof for this circuit or the specification.

>> Does it help you identify where the issue is, or is that other tools that you need to use to actually find the problem? >> It gives you a compiler error, right? Just like a just like compiling Rust code, like it when you when you're compiling a Rust Rust code where the types don't don't match. Like you're trying to add a number to a Boolean. And then we it tell you that this this is not right. Right? Like there's an error here. And it's essentially the same that happens in in in D. It's just a way more complicated type system, but it will also just tell you, "Hey, there's a type error. That thing doesn't compile." And the process of compiling as as Giorgio said that that corresponds to checking all of these proofs.

>> I I think like there were some probably other puzzles where you maybe were more in the line of the specification is not correct. And that's something that Clean would would not find because this is the responsibility of the person that writes the circuit or the specification of a circuit. >> Okay. >> If the specification is incorrect and talks about the wrong thing, then you're done. Uh it it works like it's sound, it's complete, but it's the wrong thing. >> So is it's looking Clean then is looking for engineering problems, like implementation issues?

>> Mhm. >> In like from spec to code, it's supposed to match up. And if there's a discrepancy in the coding in the actual like building of the spec, it'll flag it. But if the spec is weird, you can build exactly the correct version of that spec, it still won't work the way it's supposed to because there's a problem with the spec. >> Exactly. >> But Clean or Lean will just say it's fine. >> You're proving equivalence, but obviously if if the if the if the thing you you're you're running is equivalent to something that's buggy, then that doesn't help you. But but as Giorgio pointed out, the advantage is that the spec can be a lot more readable.

Like it it can look like regular code. In so far as like Lean looks like regular code, but like it can have like loops and and bitwise operations and all of these like nice high-level things. Operations on integers of arbitrary size, all of this nice stuff. So for instance, you can write a SHA-2 spec in like a couple hundred lines, maybe. But when you go to implement the circuit, that's much much bigger, especially if you want a nice optimized one. >> Got it. >> Mhm. I was going to say, keep in mind people have been tinkering with, you know, polynomial constraints one by one literally touching the polynomials instead of writing, you know, code. So, especially if you're doing like a ZK VM for example. So, these circuits are super complex and it makes sense to want to read something that's a lot smaller.

>> Yeah, and not not not only that they're super complex, they're super complex not just because people like to make things complex, it's because efficiency in snarks depends a lot on the number of constraints and you sometimes also want to use this non-determinism aspects of of our proving systems and that is not usually the natural way that you would write programs and writing circuits is much lower level than writing assembly and even assembly is hard for people.

Yeah, this is where this asymmetry that you guys described is really nice because your specification can look like a program and that is what we are used to write as engineers. >> Another advantage is that I mean a specification is just some description of behavior and maybe maybe you don't need to write it yourself. Maybe you can find somebody else who's already written a specification or you can prove your specification equivalent to that specification. So, a big example is for instance there is a specification for the risk five CPU. Right, so you don't need to write a specification for risk five. There already exists one. You can just take that one and prove that your ZK VM the the very complicated circuits

that that it uses that those are equivalent to this specification then that a lot of people have already looked at. So, then you don't need to look at all these circuits, right? You just look at this high-level specification. >> Let's continue on the sort of story of ZK Golf. We now are we're familiar with clean, your sort of extra DSL on lean that focuses on circuit sort of proving circuits are correctly implemented. Where then is the ZK golf part? Where's the competition? Like I'm kind of now I now I'm like, oh, this is a cool tool, but I just I still don't know what ZK golf is.

>> ZK golf didn't happen because so once once once an LLM can write a circuit, it it maybe maybe it can also write a better circuit. So I I had this idea that I would ask the LLM to also prove that the circuit it comes up with is R1CS. So in in in clean, a circuit is just arbitrary equations that must be zero all of them. >> Mhm. >> So it can you know, they can have arbitrary form. So I restricted to R1CS and I have the LLM also prove that the concrete circuit is coming up with is R1CS. And I have it prove how many constraints it is.

So I ask the LLM to like tell me how many constraints is this circuit that you're building and also by the way prove that that is the number of constraints that it is. And then I tell it, this is how you measure cost. You measure cost by taking the number of like witness cells and constraints and summing them up and that's the cost measure that I that I use. And then I put Claude in a in a goal loop for two days and told it to drive that cost down without changing any of the central definitions. >> Okay. Is like the LLM using clean? Or is it coding? And then you're running clean on it to see how good it is.

>> So I'm fixing the definitions so it can't change the definitions. It can't change what it's supposed to do. >> Okay. >> It just means that I'm fixing some files in a in a project. And then I'm asking it to write a bunch of lean code using clean. >> Okay. >> As a library. Yeah. So that that's that's how it works. And I'm asking it to drive down this theorem that that tells you how to measure the cost of a circuit. >> When you say definitions, do you mean like the spec of the circuit we care about? >> Yes. So this the spec is fixed and the definition of what R1CS is and it need so it needs to prove then the circuit is equivalent to the shot to spec. So, basically what what George's example had had already had already proven.

And then it also needs to prove that the circuit is actually almost yes. So, I think originally George was just inspecting the circuit and checking that it was almost yes indeed. But now I I I I'm going to ask an LM to to write the circuit. So, I can't really trust it to not screw with me. So, I'm going to ask it I'm going to have it prove that it doesn't, you know, do some sort of high degree constraints. And then I'm going to have it prove that whatever cost it's telling me that this circuit has, it is actually the the cost that it has. I'm I'm asking it to grade its own homework, but it has I'm going to verify that it, you know, graded correctly. It's going to prove that it graded correctly.

>> So, then what is the competition though? Is it individuals trying to reduce the cost of the clean code? Like that's the part that I'm a bit confused about. Like I get that you So, you've identified there's a cost associated with I don't know if it's the compiling of a circuit or like the action of a circuit and you're trying to reduce that somehow, but I I'm I'm sort of not clear on how like writing formal like how formalizing it by using clean like somehow is connected to cost. >> So, you when you write a circuit in clean, right? You're writing a bunch of constraints.

>> Mhm. >> And I'm just asking it to prove like how many constraints there are basically and like how many witness cells there are. That's all. Like it it comes up with the circuit and I would like to measure it, but if I if I if I need to run my circuit then it requires me to run lean code and you generally don't actually really run lean code. You just compile lean code. >> Okay. >> So, instead I'm going to have it prove what the what the cost would be. But essentially I'm just measuring the cost of a circuit. This is this is prior to CK Golf by the way. And it was kind of like a dumb idea and I think I think George didn't expect it to work. I kind of didn't expect it to work.

>> Yeah. So, >> [laughter] >> so in some sense people or AIs I guess do two jobs. They both write circuits, which the circuits themselves are usable outside, but they also write the proofs of correctness. So, are these circuits that are written in Glenn directly transferable to other places? >> I mean they they wouldn't be transferable if they were not R1CS, right? So, that's that's exactly why we need to like restrict it a bit so that it's not like during it's not it's not new So, a circuit is as as I said just a bunch of constraints of like any any degree, right? So, we want to restrict it to be like degree two and factor into two linear combination. And then you can export these constraints and prove it with whatever prover you like. Yeah,

we're we're kind of getting ahead of ourselves, but but there is no way to basically just like export the circuits out and get a get a Groth16 proofs or something like this. >> Hmm. So, have we have we actually explained ZK-Golf now or is there another stage or step to the competition to make it a competition? >> So, this this is a dumb experiment where I I ran this for a couple days and then I expecting it to spin and do nothing, but then when I came back it actually produced at that time the the best SHA-2 circuit, R1CS SHA-2 circuit. And that was like very surprising for us at the time and I think that was kind of like when the when the penny dropped.

It's like, "Okay, not only can these can these LLMs write circuits, they can also write really really good circuits because you can just put them in a loop and ask them to drive down this measurement of cost and eventually you will succeed." >> Did it end up writing something you actually already knew? It like did it find the solution you wanted or did it find a better solution than you expected? >> It It found new solutions. So, it started by trawling the internet and finding all of the existing tricks and applying them all together in one implementation. And that already got it got it down, but then it found genuinely new techniques.

>> Oh, crazy. Okay, and then you would have seen like you would have looked into what it did and then been like woah this is not something we've seen. >> You don't have to but you can. >> Okay, so is this CK Golf? >> So at this point I think I think George >> [laughter] >> George came up with this idea that like uh we I mean this is sort of semi-trusted, right? Like but in in practice in in theory you don't need to trust any anyone. You don't need to trust the LLM to write any of this because the the circuits are untrusted, the proofs are untrusted. And so in theory you could just have arbitrary people around the world supply circuits and then prove that this circuit that they supplied is is better and still correct.

>> Wow. >> And that is essentially the the brain seed of of CK Golf. It's what if what if anyone could write the circuits? Yeah. >> do see >> Yeah. >> Here you do see a little echo of the Yukon or kind of type competitions because as far as I understood there's it was like the goal is you have to create a very like well-posed question. It has to be quite like boxed in like what you're trying to optimize, what you really want. Because if you make it too vague, there's all these workarounds but you might not actually end up with the outcomes you want. But in your case like you've basically made made it very clear that like here's the language you're going to use, you're going to build a circuit, these are the constraints, you're going to find a cost associated with them. Or actually I guess you don't

give them constraints, you're just saying like there will be constraints. There will be a cost, you're trying to drive down that cost. But like it sounds like you kind of boxed in the problem. You've like made it very specific so that you can run this stuff. >> 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. >> Have you seen any like any competitors agents go rogue and like just start like breaking stuff? Like you [laughter] know like making a message board in the circuit that like shares secrets and like somehow or like I guess it would be really hard to do because you're using lean, right? Like you'd have to sort of break lean to work around it.

>> So we we we did find a couple of there was there was a couple of bugs in in CK Go in in the relatively early days. The first one was was pretty dumb. So it was that I was asking people to prove the cost of their circuit on a default input. So I you have to prove that you know, when I take your shot two circuit and I plug in, you know, zeros then it has whatever cost it has. >> Mhm. >> And then essentially somebody just submitted a circuit that branches on the input. So you it's since the input is a constant, you can branch sort of at compile time, right? You can say hey, if this constant that is zero now, if it's this if if it's actually zero, then my circuit is the empty circuit or and it and and it

just outputs, you know, constant shot two of of zero. >> Okay. >> If the constant is not zero, then you know, I give you an actual circuit. So then you can still prove soundness because you prove soundness of the actual circuit. But the cost when I go to measure it is zero. >> Okay. >> So it's not really a bug in in clean. It's it's a bug in my uh cost. >> in your in your problem statement or your competition. Yeah. >> Yeah. >> Was that actually a user who did that or was that a like an LLM who discovered it, do you think? >> I think it was a it was a bunch of users who were intentionally trying to screw with the thing. Yeah. >> Okay.

>> [laughter] >> But yeah, have there been any other kind of bugs found or like workarounds? >> There was another thing which was actually the bug in in clean. Oh wow. Or actually it was like clean was not originally intended to be used with adversarial circuits. >> Ah. >> And and there was like another side in the completeness definition. Because you you you know, in the submission you have to give a circuit which is just a an object. And you can just think of a circuit as like a fancy way of defining a list of constraints.

And you have to provide a proof for soundness and completeness and other stuff like soundness and the cost. >> Mhm. >> So, if the the soundness theorem statement fails to so that if there is a bug, you can basically write a zero cost circuit because of course you don't have to enforce anything, right? >> Mhm. >> So, it can be under constraint and so you don't enforce anything. So, the number of constraints is zero. >> Okay. >> But more subtly, if the completeness statement has a bug, then suddenly the unsatisfiable circuit is sound for any specification.

>> Mhm. >> Which is kind of kind of counterintuitive, but the verifier that always rejects is sound for any specification, right? Because I don't accept any false proof because I don't accept proofs. >> [laughter] >> For every proof that is accepted, you know? >> It's okay. >> Yes. Yes, that's I mean, but when you do formal verification, you have to kind of be very precise about statements. And so there was a way to define like a self-referential or like self-contradictory uh witness generation function. So, the witness generation function is like a way to prove So, if you run these functions, you get a satisfiable assignment. And so it's a fundamental object for completeness because completeness assumes that you run this

function and if the this function is like self-contradictory, you get a false assumption in the theorem and then you can trivially prove completeness. And so if you can bypass completeness, then the you can just write submit the unsatisfiable circuit which is sound for any specification. >> Mhm. >> And so there was this other break. But I want to mention that both times this was kind of a limitation of how do we check stuff because Lean again was not designed for adversarial proofs.

>> Yeah. >> And so it it it was really designed for ergonomics, for really for mathematicians. >> Yeah. >> And for example, one of the things we cannot do is run Lean code. So, we cannot, for example, run tests. We cannot export the circuit. But, if you were doing this for real, like if you were like actually developing a circuit and optimizing it with LLMs, it would not only do formal verification, it would try to export it, it would try to run it, it would try to prove on some instances that this thing actually works. And both exploits could be caught by just running a test.

>> When When you discovered like each of those kind of like workarounds, what did you What did you have to do? Did you have to like change clean? Did you have to fix something? Did you have to make it so it could sustain more adversarial use? >> The The first one was extremely simple. It's You know, I I I I don't ask you to prove the cost of your circuit for a particular input, but I I ask you to prove your cost the cost of your circuit for every possible input. >> Okay. >> And uh yeah, that was an easy fix. >> And for those that had to do with clean? >> Uh so, we were actually aware in clean that this was an issue, but it was not in practice because human wrote circuits.

And so, it was kind of a very contrived with transgeneration function that you had to write. And you know, it was unlikely to happen. And so, now with ZK-Golf, we we require some additional property to rule out these self-contradicting with transgeneration functions. >> Have there been given the renewed or I guess there's been interest in Lean for a long time, but really in the last 6 months, a year, we hear about it a lot. We've actually done a few episodes on the topic. I think Wyatt Benno mentioned it.

And then we did an episode with Alex Ozdemir, like very much about Lean. So, I'll link to that in the show notes, but like has Lean had to be battle-tested itself? Like you're building on top of it, but has any other kind of like maybe not only in our space, but in generally in the world, has there been kind of some vulnerabilities found in the language? Have you had to fix things or is it's I'm assuming it's still being worked on? >> There've been a bug in in in the leading kernel itself where you could prove false. So, I mean, if you can prove false, then you can prove anything. >> Yeah.

>> That's a that's a that's a bug. >> Big bug. >> Well, it's kind of a rite of passage, I think. Rock also had similar bugs. It's just It's happened to many of these type checkers. It It's like you can you can write one program that miscompiles and >> Mhm. >> then you fix the compiler. >> Yeah, okay. >> So, I'm curious about the current state of ZK-GOLF. I wanted to ask you guys what kind of circuits do you have up for competition? And have you seen any trends in how people compete and maybe what models they use and what results they get?

>> So, we have SHA-2. Uh Oh, so So, first of all, most it's it's worth mentioning we started out with with just prime field circuits over the BN254 curve. >> Mhm. >> And we started out with SHA-2 and some Bitcoin curve operations >> Mhm. >> as well as the Keccak. And all the circuits for for all of these are by far the best out there as of so good stuff that are out there. >> As in ever in the world? >> As of ever. Like, I think the the fixed based foreign field So, I mean, it's the Bitcoin curve and you're emulating that one over the BN254 curve.

So, we have to do field emulation, which is super easy also to to write in your spec because it's just You're just doing operations in in some other field, right? You don't care about like the field of of the of the of the SNARK. So, it's super easy to write, but it's obviously super hard to to implement. If you've ever tried implementing this foreign field emulation, it's extremely complicated because you have to keep track of limbs and and norm bounds and all kinds of interesting techniques like entity and the CRT decompositions and all all all all kinds of tricks that people have been using to try and drive drive these down. So, I think at the moment the fixed base scalar multiplication on the Bitcoin curve is I think seven times better than the previous state of the art. So, seven times less constraints.

>> It's It's extremely optimized. It turns out that the that the previous state of the art, which was like I think it's circom ECDSA, is is already is already pretty optimized. Like it it's not a naive implementation. It's It's already pretty pretty clever. But there's there's a lot of room for for improvement. >> I just realized when you are saying circuit, it could be all kinds of circuits. But like is there like a lot of ZK circuits specifically in this competition, ZK Golf? >> [laughter] >> So, on ZK Golf we have just ZK circuits. And the the way that ZK circuits differ from, you know, regular circuits is that they're a non-deterministic, right? So, you can you can witness values, whereas a regular circuit is a is a function, right? Like you take an input and it

delivers and it computes through it and delivers some outputs. >> Okay. >> So, that's that's the primary way that these circuits differ from deterministic circuits. But in principle, yeah, it could be you could do the exactly the same for circuits. >> But I don't really understand which part of a ZK like So, I'm I'm just thinking of like a ZK proving system, maybe more largely. What part are you actually optimizing? >> The number of constraints. >> Okay. >> So, we basically ask people to submit a a circuit and then prove that then they tell us this is the number of constraints my my circuit has a a thousand constraints and it uses a thousand witness cells.

>> Yeah. >> So, a thousand rows and a thousand columns in in R1CS. >> And by making that lower, you're making it faster, cheaper? >> Yes. >> Okay. And why are you like this is actually a question maybe for the ZK security crew here, like you guys are doing lots of audits, but is this like what is the contribution here? Is this to audit? Is this helping with audits? Is it helping your clients? Is it your own pet projects? Like why are you optimizing circuits? >> [laughter] >> It's all of this. So, I I think in in in terms of contributing to the wider community, obviously we get some really nice optimized circuits. I think the author of of Gnark has already upstreamed a bunch of the the circuits for the

Bitcoin curve. >> Cool. >> So, you get like more efficient easy recover inside your circuits. But, in addition to that, I think it's also very clearly the direction that authoring and auditing CK circuits is going in. >> Humans are extremely bad at at being extremely careful for extremely long time. >> Yeah. >> And it turns out that that's essentially what you need to do to write a correct CK circuit, right? You have to a single a single missed constraint means that the whole the whole thing is is is is broken. And it humans are much better at like writing and reading high-level things and then asking machines to to produce the very low-level implementations.

>> Mhm. >> So, I think both in terms of being able to develop faster because you just write a SHA-2 implementation or take one that already exists and then you just ask an LLM to produce the circuit for you, which is much faster than writing it by yourself. >> Yeah. >> But, also in terms of security, yeah. >> If you were doing an audit for a company's proving system, would you then include it in something like ZK Golf? Like, their their spec and see if people could prove like cuz then aren't aren't you just doing optimization work for that company? Which is cool, but I don't know if that's what you're hired to do.

Maybe you are, I don't know. >> There's there's two things, right? Like, if a company comes with a the circuit, then the first thing you ask them naturally is what does it do? >> Okay. >> Right? Like, what is what is this circuit supposed to do? And then as an auditor you take a you take a look at the circuit and you verify that it it it does what it's supposed to do. >> Mhm. >> But, obviously if you can tell me formally like you tell me exactly what it's supposed to do. Like, is this supposed to be a SHA-2 circuit? Then, I can also just take a SHA-2 spec that I have or I can write one. >> Uh-huh. >> And then I can ask an LLM I just like use a lot of effort to have it prove that this circuit that you brought me is

equivalent to the shot to respect. And at that point I I don't need to look at any of the constraints. I just look at the shot to code which is much easier to look at. >> But here's not a competition. This is just you're using clean. >> That would be an example of using it in in an audit or to like formally verify a circuit that you already have. >> Okay. >> Or even better if customers show up with the ZK golf circuits unmodified then [laughter] you know that then that's done. >> Then you know. >> Yeah. >> Very nice. >> Yeah, I mean there are a lot of circuits that have been written by hand across the ecosystem and like like we said in a sec it was a necessity, you know, doesn't have to be the case anymore and you can have them to be to be secure

which is really nice. >> When I covered the Yukon platform we talked about a few different competitions that they had over there. So they had ECDSA dot fail, snark.fast, and better.codes. What is ZK golf similar to? Like how would you categorize it? >> So ZK golf is is most similar to better.codes which we also collaborated on because better.codes is also using formal verification. Essentially you asked to write a formal proof like a lean program and then I'm type checking it. Essentially you're grading your own homework and then I'm checking the grading.

Whereas a bunch of the other Yukon Yukon competitions are you sent me a program and then I run the program on some system or I in an emulator and then I measure what it costs. >> Okay. >> Like in one in one example you give me a program I run it. The other one you you tell me how good your solution is and then you have to prove that that it is as good as you you you say it is. >> Nice. So you also collaborated on better.codes. Maybe we can talk a bit about it because we covered it in the Yukon episode but we actually didn't go as in depth with that example as we had with the other ones. So this is I know related to the proximity prize that was first announced by the EF last year on the show actually. Justin mentioned it then. But

then it seemed and it seemed like right around that time just through my work on ZK mesh I was seeing so many papers coming out trying to solve this problem. But the problem didn't seem to have been fully defined at the time. So like there was amazing research coming out but were they really in the competition for the proximity prize? It wasn't exactly clear. At this point have they formulated the question very clearly and that's why they can run something like better.codes? >> Yeah, I think like even before we go into the details of better.codes, maybe just to even make the the link of ZK golf and better.codes compared to the other competition of why why they are similar.

I think we discussed this in the episode with Benedict where we dis- we covered okay, now we have AI's LLM collaborating with us and producing stuff. But how do we know it it's correct? >> Mhm. >> So we talked about this kind of like concept of anchors of how do you verify the result is correct? >> Yeah. >> And in some competitions out there or some work that people are doing, you have some nice anchors. Okay, you run this function if this function returns true you're fine. That's good. >> Mhm.

>> So for example, a hash stays the same of something. So I think some some of the UCAN competitions look like that, right? Like you have StarkNet Fest where the verifier of flock stays the same. >> Yeah. >> So if the verifier stays the same and you just keep optimizing the prover, then you're good. >> Assuming that the verifier is acting correctly, it will only verify a correct proof from a prover acting correctly and so you're sort of using that that phenomenon to say we don't have to check actually what the prover is doing as long as it's accepted by the verifier.

>> And it can do whatever you want. Can use GPUs, it can use like cash look up tables, whatever it wants. Just do it fast. I don't care. You do have to check some other properties or like completeness. You do have to kind of get a feeling that it is going to also for every correct input you you also want it to be able to produce proofs for everything that it should be able to produce proofs, but you you can reason about it in other ways. But the most important part is that the soundness or the verifier stays the same. So, that's fine. So, that's like one sort of anchor that you can have.

And the anchor here in ZK-Golf now was more about Okay, do we have formal proof of correctness? And better than codes in that way like Matias said is very similar in that regard. And the problem in proximity prize, there is a paper that described it. And there is a very nice library that has been written in collaboration with I I think now it's many people in the industry, but spearheaded by the Ethereum Foundation, which is called arith lib, which describes in Lean all the ingredients and all the fundamentals that are needed to describe problems in coding theory, finite fields, all the

different parts that are needed to describe proximity prize problems. And now you have arith lib, you have people in the area for example Alex Heinrichs that works a lot on this, and you have the proximity prize paper that describes these grand challenges that have to be solved. Like can you improve something about these grand challenges? And you know, the problem with stopping there with the paper is that okay, this this is nice. Like you someone can go write a paper say okay, we improve the the results about the grand challenges.

>> Mhm. [laughter] But that's hard. That's that's theory. It doesn't relate to some concrete problem. >> Mhm. It's also not clear like at which point like is a threshold met that >> Yeah. >> it would be accepted. Because I what I was seeing with a lot of the papers was like in certain conditions they were able to either prove or disprove the things they were supposed to do. >> Exactly. >> But that threshold of like conditions was not defined. So they could just like describe like scenario around the problem and then find ways to prove within it. But yeah, that wasn't quite standardized. And so I'm hoping is better.codes standardizing it then?

>> That's so exactly. That that's that's I think a great point to make which is what you made which is that So what the idea was in better.codes was that the designers of these challenges what they said is the following. Okay, we'll take a concrete problem. Let's choose the finite field. Let's choose the size of the message. Let's choose the specific code that we're looking at. Let's choose the parameters of that code. Let's choose everything. >> Mhm. >> Let's make it very concrete.

And let's have the solvers collaborate on improving the bounds for this specific toy problem. >> Yeah. >> And the hope was is that the improvements that are done for this toy problem would translate to more generic improvements for these grand challenges. There was always the situation or there was always the chance that the improvements that would have been made were only specific to this toy problem. >> Yeah. >> And this finite field and whenever you change the finite field then that that that's it. You're done.

>> And what has happened? Cuz it's running now right? >> Yeah, but what what we've seen is that the designers were correct. Actually the results of the solvers were generalizable to to more general ideas that can be applied for these for these challenges. But it was a long road. I think like for some time, it has been the case that the AIs were just collaborating just to get the results formally proven for what we already know. >> Oh.

>> And then it was stuck for like a while. >> helpful. >> Yeah. Yeah. >> Yeah, it's helpful like as a base, you know? Now we have a base that we can work out of. Maybe when someone writes a new paper, they can use this as a base to to write their new proofs. But then it was stuck for like about, I think, 6 days. The AIs were still thinking but not finding a solution. Until the the U Conn team invited one of these top researchers. Yeah, exactly, Bar Dos. He came by and joined and I think it was posted that he said, "Yeah, I I I don't think it's doable but I'll try." Within a day, his system managed to find the an improvement that just crossed the

threshold by just a bit. But it crossed the threshold of what was already known in the state of the art. And since then, it has been improved even further by the AIs. >> Okay. >> And a bunch of papers have been written already that credit their ideas, or at least some of their ideas, to be inspired by this small jump. >> Wow, that's so cool. >> We see something similar on CK Golf, right? Like one agent will come up with a trick and then all the other agents would like take that trick and just like apply it everywhere and also try to like come up with incremental improvements. So it's like there'll be like one big, you know, discovery from one agent and then

everybody else will just pile on. >> How do you incentivize things in CK Golf? Do you have sort of similar monetary gains or can you like monetary prizes at snapshots or is it just for the cred? >> The cred. There is absolutely There's absolutely no prizes. >> I see. >> But I mean except getting all of us better circuits, right? So I mean the circuits are widely available to to anyone. >> Although you never know when a challenge is a hiring challenge. >> [laughter] >> Yeah. Going back to that. I mean that's what we had seen kind of unexpectedly from the ZK hack puzzles that it became a hiring funnel.

>> Exactly. >> And you talked about the CTFs that got you or kind of being in the CTF world and then doing a puzzle got you hired Giorgio and you as well Matthias. I mean but here it's different, right? Cuz it's like how good are you at taming your agent? >> That might be the profession now. Who knows? >> True. I think Bartuš is going to get hired. Uh he's already working I think at a university [laughter] but Interesting. >> I guess one thing I didn't mention about ZK Golf is that we have since added binary challenges. So a particular challenge circuits that are suitable for for Flonk.

And also there we've seen some improvements especially on the SHA-2 and and and Blake Blake 3 circuits that are much better than the existing circuits that we used in Flonk. >> How many kind of circuit types competition like are there separate competitions within ZK Golf for different kinds of systems and how many are there? >> Every circuit is its own little challenge. >> Okay. >> So you can you can win you know the specific circuit on the specific field. Uh so far they they fit fit into two different types. So they fit into the large prime field case which is the one where we've seen the most crazy tricks because of the large field you can you can do some some crazy stuff. And then we have the binary field one which is this we call it canonical R1CS. So Flonk is fastest if if the R1CS has a specific

form. So yeah. It's R1CS over large prime fields and it's R1CS over binary fields. >> Okay. What's next for ZK Golf? Like will you just continue to run this? Do you have plans to expand it? Will you do more collaborations? Like, cuz I I was just thinking with better.codes, wait, is that also formally as formal verification as well? >> Yes. >> Cuz I'm almost wondering if like the ZK-GOLF could like be the counterpart of other existing competitions, but with the formal verification. >> I mean, for for ZK-GOLF, our goal is to create a very nice standard library of circuits that are extremely optimized that anybody can just like pull down and and use. So, if you're

designing a new proof system or something and you you need a SHA-2 circuit, you can just use the one from from ZK-GOLF and it will always be the best one and we'll we'll package it up in a nice way and sort of and sort of clean. And then we plan to add more challenges as we go. We still need to add some pairings and stuff like this so you can do, you know, your recursive snarks. So, >> Do you think you'll ever actually though find the final version or will it like forever be improving? >> The competition will remain open forever, but I mean, there is some best circuit, right? And so, the question is whether we will ever find it. >> So, there are circuits which are clearly not improvable. For example, like, you know, in in in R1CS over large prime fields, a range check,

they they cannot do better than witnessing the Boolean decomposition and then a final constraint a final linear constraint to like reconstruct the value. And this is actually provable with some effort. So, you can state like theorem that says, for every circuit that's probably matches the specification, so the specification is just this value is less than two to the something. For every circuit, the cost of that circuit is not less than this one. All right, so this this will give a a lower bound on the cost of the circuits. So, that that's like another very interesting direction, right? So, if I if I have this primitive, right? This range checks can the lower bound on cost of range checks is this.

My circuit, I managed to prove that they require at least 25, I don't know, range checks, then I have a lower bound on the cost. And so, we could have like a upper bound, which is given by the best circuit, and a lower bound, which is given by, you know, you cannot improve on this. But, the typically the lower bound is much, much harder to prove. >> Mhm. >> So, the higher bound is just, you know, the best circuit we have. >> Cool. I think we now better understand what ZK-GOLF is. So, thank you so much for like this journey. You know, I had to I kind of kept asking because I wanted to to get to the core of it, and I think we found it. But, now I sort of wonder like, is there something beyond ZK-GOLF, these kinds of competitions? Like, have

you been brainstorming internally for other projects? Have you seen other things? Like, obviously we're we're tracking the Yukon stuff, we're we're tracking ZK-GOLF now, but is there are there anything else that we should know about? And is there anything else that you're thinking of building? >> I mean, in in theory, you can drive down as long as you can have a measure of cost, and you can define the properties that the solution needs to satisfy, right? You can optimize just about anything. So, one other possibility could be a proof system, right? You can say, "Hey, can you design me a STARK in the IOP model that has this level of soundness?"

And then try ask me to drive down the number of queries. So, you could also be golfing on on proof systems. >> Cool. >> IOPP.golf. Yeah. >> Exactly. [laughter] >> I think another interesting direction is understanding these results and these high scores. So, we're seeing it with better codes, where people have been writing papers now and crediting ideas and starting to digest, to use sort of a bit of slang from these days, digest these ideas. We could start to do the same with ZK-GOLF. 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, you know?

>> Although, wouldn't LLMs just do that, too? >> Not in the same satisfying way a human does it. I think there is still something in getting to the core of the idea of why the circuit works better, or why the specific code proof technique for the code works. And I think humans will still explain this, at least for the time being, better than models. We can revisit in a few months. >> Yeah. So, Kobe, I also wonder, do you think we'll ever see the ZK hack puzzles make a re-emergence? Because they really I feel like they were so of their time, but you can't really run them the same way now.

Have you had any thoughts on that? >> Yeah, I think like that's a valid problem in the sense that, like we said, the one of the main goals of ZK hack was to get people to understand it. And if you remove that part, it misses the goal. Like, we want people to break the schemes so in order to understand it, not just to have the check mark, right? Yeah. >> Or to win the prize, cuz we like speed racing. >> Yeah, exactly. And the write-ups are the same. We want people to do the write-ups so in order for them to be able to understand them, maybe win a prize. So, I think that definitely they need to be changed because now the same kind of challenges very realistic, unless

they're very obscure, since they're still learning tools, they can be solved by the current LLMs autonomously, or with maybe some guidance. The question is how you can design new kind of challenges that still allow you to understand. And I think there there might be an angle which may be interesting to explore of okay, in this day and age where people write code and explanations using AI, what can go wrong when you do that? And in what common ways it can go wrong and in what ways you can even fool the AI's into doing the wrong things.

Especially in the realm of cryptography. So that might be an angle to to try out. >> Prompt your own agent to go awry somehow. Like to find to trip to trip over the tripwires that have somehow been set for it or >> Yeah, and you know, there is like the angle of like prompt injection but maybe it would be some other angle so like cryptography vulnerability injection. I don't know. You can think about all these kind of things. >> Huh. Yeah, there's maybe there's something there for us to explore. I don't know. Maybe one day ZK hack will rise again.

>> I I feel like that there is a potential future for puzzles and CTFs in different forms to rise. We'll see. >> Yeah. I think that brings us to the end of this episode. I want to say thank you so much for all of you for coming on. How do people get involved with ZK golf or with clean? >> So if you're interested in hearing more about clean, we have a wonderful website which also has a great tutorial on getting started for average developers who don't know like lean or formal verification ahead of time.

>> Mhm. >> So you can find that at clean.zksecurity.xyz. >> Cool. And ZK golf? >> ZK golf is at zk.golf. >> Do you think listeners of this show should go try it out? Should they participate? Is it really open to anyone or have all of the competitions right now been solved? Like yeah, how active is it? >> It's it's still pretty active. For for about a month we had the the challenges plateauing and then all of the sudden we saw a great influx of of improvements again. So >> Cool. >> Just when we thought we'd hit rock bottom apparently the bottom fell out.

>> Cool. >> So and we're taking suggestions for circuits as well. So, if you're interested in this, you should join our Telegram group and give us suggestions for what circuits you would like to see formalized and optimized on CK Golf. >> Very cool. All right. Thank you, Matthias and Giorgio, for coming on. Nico and Kobe, thank you for joining. Yeah. >> Thank you. >> Thank you all. This was super fun. Thank you. >> Thanks a lot. >> Cool. I want to say thank you to the podcast team, Henrik, Rachel, and Tonya, and to our listeners. [music] Thanks for listening.

>> [music]