zkGolf – Competitive optimization of formally verified circuits
Zero-Knowledge Proofs (ZKPs) let an untrusted proved show that computation was executed correctly without revealing the inputs to the verifier. However to prove anything, the computation first has to be expressed as a circuit: a system of polynomial equations (constraints) over a finite field. Circuits are the assembly language of zk and every constraint costs prover (and sometimes verifier) time, so production circuits are aggressively hand-optimized. Over the last months, we have been experimenting with writing formal specifications instead and letting LLMs produce the circuits: as long as…
In plain words
zkGolf is a tool for optimizing zero-knowledge proof circuits by combining formal verification with LLM-assisted circuit generation. Instead of manually hand-optimizing polynomial constraint systems, users write formal specifications and have language models produce the corresponding circuits while proving correctness. The approach targets reducing constraint costs for both provers and verifiers in zero-knowledge applications.
written from the facts on this page · September 2026
From the sources
In the maker’s words, at launch
Zero-Knowledge Proofs (ZKPs) let an untrusted proved show that computation was executed correctly without revealing the inputs to the verifier. However to prove anything, the computation first has to be expressed as a circuit: a system of polynomial equations (constraints) over a finite field. Circuits are the assembly language of zk and every constraint costs prover (and sometimes verifier) time, so production circuits are aggressively hand-optimized. Over the last months, we have been experimenting with writing formal specifications instead and letting LLMs produce the 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 few hours 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. We then asked the LLM to aggressively optimize the circuits, by driving down a cost metric of the circuit (number of constraints). 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 result was a (non-deterministic) circuit beating the current, human optimized, state of the art for SHA256 compression. This experience lead us to create "zk.golf" which is an open competition to produce optimized, formally verified circuits to lower the bar for the use of ZKPs and make their application more efficient. Come play (https://zk.golf/llms.txt) and learn about formal verification.
Does the same job
all alternatives →- GCGoldbach Conjecture up to 4*10^18+7*10^132025 · medium.com · ▲244
Achieved a new world record in verifying the Goldbach Conjecture using grid computing, by extending the verification up to 4 quadrillion (4×10¹⁸) + 70 trillion (7×10¹³). My grid computing system - Gridbach is a cloud-based distributed computing system accessible from any PC or smartphone. It requires no login or app installation. The high-performance WASM (WebAssembly) binary code is downloaded as browser content, enabling computation on the user’s browser. [Website] https://gridbach.com/ [Medium]…
- FIfilippo.io/mlkem768 – Post-Quantum Cryptography for the Go Ecosystem2024 · words.filippo.io · ▲315
- ZKZero-Knowledge Proofs in WebAssembly2019 · zkwasm.kobi.one · ▲81
- IBI built a toy TPU that can do inference and training on the XOR problem2025 · tinytpu.com · ▲134
We wanted to do something very challenging to prove to ourselves that we can do anything we put our mind to. The reasoning for why we chose to build a toy TPU specifically is fairly simple: - Building a chip for ML workloads seemed cool - There was no well-documented open source repo for an ML accelerator that performed both inference and training None of us have real professional experience in hardware design, which, in a way, made the TPU even more appealing since we weren't able to estimate exactly how difficult it would be. As we worked on the initial stages of this project, we…
- ACA Clojure implementation of logic programming language in SICP2019 · github.com · ▲56
- AAAsciiDots – a 2D esoteric language inspired by circuits2017 · github.com · ▲148
More work this month
the category →
The app store for voice native apps that lives in your notch
Work · 28d ago · voiceos.com
Mac-native app for screenshots, recordings and collaboration Discussion | Link
Work · 5d ago · producthunt.com
Launched alongside, July 2026
the whole month →- IR
I might be the only SRE on Earth with his own bowling center. It's a more in-depth gig than you'd think. My family and I bought an abandoned 8-lane bowling center in the rural mid-west. In our small town there weren't many recreation options for families. You've heard of a food desert? This is an R&R desert. It had been abandoned for a good reason. The roof leaks, the electrical system was constantly surging, and my 70-year-old bowling equipment (still) doesn't work perfectly. The system that keeps your score is particularly interesting to me. It's the thing you watch during your game, but…
Life & fun · Jul 2026
- EElevators▲1,680
Life & fun · Jul 2026 · john.fun
- 1W18 Words▲1,160
Life & fun · Jul 2026 · 18words.com
- BA
Over the past few months, our team has been building more and more slidedecks using web frontend technologies with coding harnesses like Claude Code, but a common complaint is to make even small edits we need to edit the code either manually or via the harness. To avoid this loop, I ended up creating Bento, a single HTML file with everything you need in a slide tool including animations and shared editing. There's no install or cloud login, everything works offline. The default deck is around 560 KB and it doesn't need to fetch anything once you got it. Open it in a browser and then you can…
Dev tools · Jul 2026 · bento.page
- GG
A few days ago I found myself trying out GLM 5.2 and was really positively impressed. The capabilities and security I was getting from this LLM are similar to those I've gotten from models like Claude or GPT, and this really surprised me. But then I thought, "I wonder how it would work on a normal computer like mine," and above all, "I wonder if it would work without going into OOM on a computer like mine." So I started working with the help of agents to test this possibility. I started converting the model to int4, understanding MTP usage, and if possible implementing DSA for long context.…
AI · Jul 2026 · github.com
