sorryfreeLast reviewed 2026-09-13
Index › Frameworks › zk.golf

zk.golf

Direct answerzk.golf is zkSecurity's competition to build the cheapest zero-knowledge circuits that are proven correct in Lean 4. Each challenge fixes a Lean specification; a submission is a Clean circuit plus a proof that it is sound and complete against it, kernel-checked in a sandbox (20-minute timeout, no native_decide, axiom allowlist). Challenges include SHA-256, Keccak-f[1600], RSA PKCS#1 v1.5 verification, secp256k1 scalar multiplication and GF(2) BLAKE3 and KangarooTwelve compression.
Maintainer
zkSecurity
Website
https://zk.golf
Repository
https://github.com/zksecurity/zk-golf-challenges
Category
Challenges and programs
Targets
R1CS over BN254GF(2) hash compression trackClean circuits
Approach
Fixed Lean interface and specification per challenge; submissions are Clean circuits plus kernel-checked proofs; score = allocations + constraints
Access
Open challenge; challenges repository public
Status (2026-09-13)
Active (launched 2026-07-02)
First public release
2026-07-02

Last reviewed 2026-09-13 by the sorryfree editors.

What zk.golf does

Because completeness is required alongside soundness, the specification pins the circuit down exactly, so aggressive optimisation, including by LLM agents (an agent API is documented at zk.golf/llms.txt), cannot silently break correctness. Score is allocations plus constraints, lower is better, and each challenge lists comparison points against existing libraries such as circomlib, zk-email, gnark and circom-ecdsa.

For a team considering formal verification, zk.golf is the fastest way to see what a sound-and-complete deliverable looks like and how much circuit cost verified optimisation can remove. A challenge submission establishes only the challenge's required properties, not the security of any surrounding system.

Where it is strong

  • Every leaderboard entry is a kernel-checked proof, not a claim.
  • Realistic targets: SHA-256, Keccak, RSA, secp256k1.
  • Designed for AI-agent participation under a fixed spec.

Limits and caveats

  • Challenge scope only; not an audit of your code.
  • Clean and Lean 4 required.
  • Young platform (July 2026).

When to choose it

Use zk.golf to learn Clean, benchmark a gadget, or recruit verified-circuit engineers. The operator, zkSecurity, runs it alongside its verification practice.

Who works with zk.golf

zkSecurity.

Top-listed for verified-circuit work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website

better.codes, Verified zkEVM program.

Sources

Last reviewed 2026-09-13 by the sorryfree editors. Machine-readable: data.json · summary.txt