zkGolf: AI, Clean and Optimising ZK Circuits with zkSecurity

Clean, zkSecurity’s framework and mini-DSL for writing circuits in Lean, aims to prove that a circuit meets a specification. Its checks address soundness, ruling out under-constrained circuits, and completeness, ruling out over-constrained ones. They do not establish that the specification captures the intended behavior: a circuit can satisfy a flawed specification and still be wrong. The proof also depends on Lean’s kernel and consistent logic; the speakers noted that a Lean kernel bug had once allowed a false proposition to be proved. In a signature-verification example, the specification was about 200 lines, compared with roughly 10,000–20,000 lines for the circuit.

The proposed AI workflow is to have an LLM generate a low-level circuit, then prove it equivalent to a higher-level program or specification, leaving people to concentrate on intended behavior. In an early hash-function experiment, generating the circuit took about four or five days and required supervision. That work led to zkGolf, an open competition where submissions must prove correctness and efficiency rather than merely produce a working circuit. The speakers said increasingly capable AI has weakened traditional cryptography CTFs: Giorgio reported that after GPT 5.5 came out, an agent solved every challenge he encountered, including difficult ones, and described asking an agent to break a paper as a new kind of CTF.

zkGolf restricts submissions to R1CS circuits and requires proofs of equivalence to the specification, compliance with R1CS, and the reported cost. Cost is measured by adding the number of witness cells and constraints. In a later optimization run, Claude worked for two days to reduce cost while the specification and central definitions remained fixed. The result was described as the best R1CS circuit zkSecurity had then seen for that computation, combining existing techniques with new optimizations. The initial run was characterized as semi-trusted, though the speaker said trust was not theoretically necessary; the competition’s aim is to verify correctness and cost without trusting the circuit, proof, or LLM.

Early exploits showed that this requires careful specification of what is being proved. One circuit branched on a fixed zero input and appeared to cost nothing under the measurement while using a real circuit for other inputs. zkGolf responded by requiring cost to be proved for every possible input. Another exploit used a self-contradictory witness-generation function to submit an unsatisfiable circuit, prompting the addition of a property to rule out that behavior. The speakers said tests and circuit export could have exposed both cases, but their setup could not run Lean code or export circuits. They also warned that a flaw in the soundness statement could admit an unconstrained, zero-cost circuit, and that Lean was built for mathematical ergonomics rather than adversarial circuits.

zkGolf began with prime-field circuits over BN254, including SHA-2, Keccak, and Bitcoin-curve operations, and later added binary-field challenges suited to Flock, with SHA-1 and BLAKE3 circuits improved over earlier Flock circuits. Emulating the Bitcoin curve over BN254 was described as especially complicated because it requires foreign-field techniques and careful tracking of limbs and norm bounds. For fixed-base scalar multiplication on that curve, the reported circuit used seven times fewer constraints than the previous state of the art. The speakers said fewer constraints generally make circuits faster and cheaper, while stressing that hand-writing them demands sustained precision because one missed constraint can break correctness.

The speakers see formal verification as a potential way to speed circuit development and strengthen audits: an auditor could focus on whether the specification expresses the intended behavior instead of inspecting every constraint. They compared zkGolf most closely with Better.codes, since both use formal verification, while other competitions discussed run submitted programs and measure cost. zkGolf’s longer-term goal is a standard library of optimized circuits, with pairings for recursive SNARKs among planned additions. It has no monetary prizes and is intended to remain open indefinitely, though finding the best circuit is uncertain: a best-known circuit gives an upper bound on cost, while proving a lower bound is typically much harder.