zk.golf: Fearless and Collaborative Optimization of Circuits - ZK/SEC Quarterly

Back to all posts

Sometimes you *can* trust the magic talking box<br>-->

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,<br>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:<br>it is just an integer modular exponentiation, with some simple checks for padding on top.<br>However, circuits implementing this functionality tend to be extremely complex,<br>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:<br>they will happily work through boring bounds analysis and equation rewritings for us,<br>and because they cannot fool the theorem prover we can trust them to do this work flawlessly.<br>This is what makes the combination of formal verification and LLMs is incredibly powerful,<br>because they compliment each other just right:<br>LLMs cannot be trusted, but are very eager to do any amount of work,<br>on the other hand, the theorem prover can be trusted, but demands a huge amount of work.<br>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:<br>we wanted to prove completeness alongside soundness.<br>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,<br>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.<br>In R1CS this would probably be the circuit with just one linear constraint, enforcing that the constant 1 wire is equal to zero.<br>This is because the unsatisfiable circuit is sound for any specification :<br>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:<br>they are called optimizing compilers.<br>For example, the Circom compiler performs a number of useful optimizations,<br>it removes redundant variables and optimizes away linear constraints.

As similarly noted in "The final form of software development",<br>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...