Today we are releasing zk.golf, a platform where people can compete on creating the most efficient zk circuits for specific problems. It is the blend of two powerful ideas:
- With Clean we are able to certify correctness of circuits using machine-checkable proofs.
- With frontier AI models, we are able to obtain deeply optimized circuits with accompanying proofs in days.
We call it fearless optimization of zk circuits.
How We Got Here
Over the last months, we have been experimenting with letting LLMs write circuits, as long as they could prove that their implementation was correct. It started with SHA-256: we hand wrote a specification in Lean for SHA-256 compression, and then we asked LLMs to write the circuit, targeting R1CS arithmetization and large fields. It took a couple of nights of work for Opus 4.7, and some light steering into the right direction, but in the end the model came up with a reasonable implementation.
The amazing thing is that we did not really have to check if the circuit was correct. Since it was implemented in Clean, Opus 4.7 provided both the soundness and completeness proofs with respect to the hand-written specification we wrote and we trusted.
After some time, we asked LLMs to aggressively optimize the circuits, given a target cost metric. We immediately got very promising results, just by asking to come up with optimization ideas, implement them and prove that the new circuit still satisfies soundness and completeness. Sometimes, it came up with unsound optimizations, however, since it could not prove them, it backtracked and got itself back on to the right approach.
The Lean kernel and the Clean theorems were happy, we were happy.
A Natural Asymmetry
Think for a moment about RSA signature verification. The algorithm can be written out in a few lines of code: it is just an integer modular exponentiation, with some simple checks for padding on top. However, circuits implementing this functionality tend to be extremely complex, mainly due to how big integer arithmetic is implemented, and the various tricks for doing it efficiently.
At zkSecurity we have reviewed many of such circuits: it can be really hard for humans to keep track of ranges, assumptions and relations between different components. However, most of the time, the correctness reasoning is boring and uninteresting: it involves simple equation rewritings, range analysis and sometimes polynomial evaluation reasoning.
These are exactly the kinds of proofs LLMs are really good at: they will happily work through boring bounds analysis and equation rewritings for us, and because they cannot fool the theorem prover we can trust them to do this work flawlessly. This is what makes the combination of formal verification and LLMs is incredibly powerful, because they compliment each other just right: LLMs cannot be trusted, but are very eager to do any amount of work, on the other hand, the theorem prover can be trusted, but demands a huge amount of work. The result is that a formalization effort that previously took years, now can be done in days.
Just the Right Circuit, Please!
In the early days of Clean, we had a distinguishing feature with respect to other zk formal frameworks: we wanted to prove completeness alongside soundness. At the time we did not realize it, but it turns out that this is exactly the feature that allows us to let untrusted users, and in particular LLMs, write and optimize circuits for us.
If we ask an LLM to optimize any circuit, and we required only soundness, the output would be surprising: it would be the cheapest unsatisfiable circuit.
In R1CS this would probably be the circuit with just one linear constraint, enforcing that the constant 1 wire is equal to zero.
This is because the unsatisfiable circuit is sound for any specification:
the prover will never be able to convince the verifier of a false claim, simply because they will not be able to convince them of anything!
By requiring soundness and completeness, we exactly pin down the right circuit, from the correct opposing directions.
What About Compilers?
One may say that we already have tools for automated circuit optimization: they are called optimizing compilers. For example, the Circom compiler performs a number of useful optimizations, it removes redundant variables and optimizes away linear constraints.
As similarly noted in "The final form of software development", writing directly in the low-level language is much more powerful:
- We are able to remove the trust assumption of the compiler correctness, and instead rely on the tiny semantical core of constraint satisfaction.
- Even if the compiler is formally verified, we are able to do specific optimizations tailored to the problem. Compilers can only do generic optimizations, which, especially in zk circuits, tend to be insufficient if we are aiming for aggressive optimization.
In a sense, LLMs + an interactive theorem prover is a very clever and very expensive optimizing compiler: converting a high-level specification (like a simple program verifying an RSA signature) into a complex low-level description (like a zk circuit).
Specifications, Not Circuits.
We increasingly believe that no one should even look at constraints ever again: constraints are the lowest level possible for writing zk circuits, and while they exactly describe the assertions made by the underlying proof system, they are not the best language for human auditability. Using the approach described in this post we can skip the review of constraints, and directly review the Lean specification.
Of course, specifications, like all code, can have bugs, however reviewing specifications is much easier: the specification is not an optimized implementation and can be written in the most natural way to express the computation e.g. modular arithmetic using integers with arbitrary precision. This greatly increases the confidence in the circuits we write and deploy, it also significantly lowers the barrier to entry: practitioners can write specifications as easily as they write programs in any regular programming language and then ask an LLM to convert it to an optimized circuit implementation with confidence using Clean.
What Is zk.golf
This post so far has been a random collection of thoughts and opinions. What did we build?
zk.golf is a platform that allows users to compete in creating the most efficient circuit possible for a given "formal interface". The interface of a circuit defines all the interesting properties of a circuit, and is composed of:
- The input and output types.
- The assumptions on the inputs, that have to be checked elsewhere, for example by the caller of the circuit (sometimes this is called the precondition).
- The specification, which is the guarantee that the circuit provides (sometimes this is called the postcondition).
For each challenge, we wrote a formal interface, which we believe represents an interesting, real-world problem. People can submit arbitrary circuits, as long as they provide a machine-checkable Lean proof that their circuit satisfies the interface. We verify the Lean proofs using comparator.
Since Clean supports lookups and high-degree constraints, users additionally have to prove that their circuit is R1CS, and they have to provide cost proofs for the circuit. The two cost metrics are the number of allocations and the number of constraints. Currently we score submissions based on the sum of allocations and constraints, and we target the BN254 prime field.
Get Involved
If you think you can beat the state of the art for zk circuits, go to zk.golf, pick a challenge and start optimizing. We have also written some guidance for LLMs to autonomously perform the optimization and submissions for you: just create an API key and point your agent to llms.txt. Even if you have never played with formal verification or Clean before, this is a very easy way to get started and to look at some simple, yet real-world examples of what specifications/formal verification looks like. You can optimize circuits by simply guiding your agents towards the right techniques and tools.
We will be adding more challenges in the coming weeks and our goal is to ultimately provide a library of highly optimized, formally verified, zk circuits for the whole community to use.
We look forward to seeing you all on the leaderboard!