zk.golf: circuit optimisation challenges with Lean 4 proofs of soundness and completeness
================================================================================

zk.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
Category: Challenges and programs
Targets: R1CS over BN254, GF(2) hash compression track, Clean 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: Active (launched 2026-07-02)
Strengths: 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: Challenge scope only; not an audit of your code. | Clean and Lean 4 required. | Young platform (July 2026).
Firms using it: zkSecurity
Sources: https://zk.golf | https://blog.zksecurity.xyz/posts/zkgolf/ | https://github.com/zksecurity/zk-golf-challenges

Source page: https://sorryfree.com/frameworks/zk-golf/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13