Ethereum formal verification challenge targets SNARK proof gaps
The Ethereum Foundation has launched better.codes, an open autoresearch challenge focused on machine-checked security benchmarks for hash-based SNARKs. The project asks participants to use their own AI agents and tooling to improve a Lean-formalized soundness bound for koalaIRS12, a Reed-Solomon proximity problem. The immediate target is a proven 128-bit lower bound, with accepted progress checked by the Lean kernel and published back to the public repository. For Ethereum researchers and zero-knowledge teams, the project turns a difficult proof problem into a shared, incremental benchmark rather than a closed academic race.Why the benchmark matters for hash-based SNARKs
The better.codes challenge addresses a gap between conjectured security and machine-checked proof in modern succinct non-interactive proof systems. The Ethereum Foundation says many production hash-based SNARKs, including systems relevant to zkrollups, zkVMs and Ethereum's post-quantum roadmap, rely on proximity gaps and correlated agreement for Reed-Solomon codes.The practical issue is not whether those systems are being used, but how much of their assumed security can be proven with formal machinery today. According to the announcement, deployed systems target 128-bit security, but that guarantee fully rests on conjectures where current proofs fall short of what researchers believe may be possible. better.codes is designed to narrow that distance through open, verifiable work that can be inspected and reused.
That makes the launch relevant beyond one theorem. If successful, the challenge could raise the public baseline for how cryptographic claims are justified in proof-system engineering, especially where high assurance is needed for systems that secure large-scale blockchain infrastructure.
The challenge centers on koalaIRS12 in Lean
The first better.codes problem is koalaIRS12, a Reed-Solomon proximity problem connected to the Ethereum Foundation's Proximity Prize research. The theorem statement, parameter point and verification harness are pinned, while solvers work inside a designated submission surface to prove a larger soundness lower bound scored in bits.The challenge problem comes from research described in Open Problems in List Decoding and Correlated Agreement by Gal Arnon, Dan Boneh and Giacomo Fenzi. The Ethereum Foundation says koalaIRS12 bridges directly to those grand challenges and is formalized end to end in ArkLib, the Lean 4 library for formally verified arguments of knowledge.
This framing is significant because it reduces ambiguity around what counts as progress. Participants are not merely proposing arguments in prose or experimental notebooks; they are trying to produce formal proof artifacts that match the pinned statement and pass verification. The result is a benchmark that can improve incrementally without changing the target midstream.
How submissions are checked and promoted
better.codes uses Lean as the final authority for accepted proofs. A comparator checks that a submission's exported theorem exactly matches the pinned statement, and the Lean kernel then checks the proof itself. Only accepted results are promoted to the public repository.The Ethereum Foundation describes the process as transparent and git-backed. Promoted submissions are credited to the solver and to the AI model used, while new lemmas, proof techniques and impossibility results are upstreamed for other participants. Past diffs and submission notes are intended to help later solvers avoid dead ends and build from prior work.
This matters because formal verification challenges can otherwise become fragmented, with private attempts producing little shared infrastructure. By publishing accepted improvements and useful negative results, better.codes aims to make each valid contribution part of a common research ladder rather than a one-off contest entry.
AI agents are tools, not proof authorities
The project is explicitly built for participants who point their own AI agents, harnesses and tools at the benchmark. The Ethereum Foundation argues that no single agentic setup is optimal across an open problem, so many independent setups working against the same verified target may move the frontier faster than one centralized team.That claim fits a broader pattern cited in the announcement. The Foundation points to earlier open challenges such as ecdsa.fail, zk.golf and snark.fast, which it says moved research frontiers in quantum circuit design, verified ZK circuits and post-quantum proving speed. better.codes applies a similar structure to a formal proof target, where an agent may search or assist, but the proof must still pass Lean.
The distinction is important for trust. The challenge does not ask the public to accept an AI model's reasoning as security evidence. It uses AI-driven exploration as a production method, while machine checking remains the gate that decides whether a result improves the benchmark.
Eligibility, awards and scope remain governed by terms
The Ethereum Foundation says today's launch covers the soundness challenge for raising the proven lower bound for koalaIRS12 to 128 bits. It also says further challenges may be added over time, but the announcement does not present a schedule for those additions.Participants are directed to sign in with GitHub at better.codes and clone the challenge repository. The source states that eligibility, evaluation, awards and payments are governed by the program terms and may be adjusted as the challenge progresses. Those details are therefore operational terms of the program, not fixed technical results.
For readers, the boundary is straightforward: the verified news is the launch of the challenge and its public benchmark model, not a completed proof of 128-bit soundness. Progress depends on accepted submissions that meet the pinned statement and survive Lean checking.
Conclusion
better.codes turns a hard cryptographic research question into a public, machine-checked leaderboard for formal proof progress. Its first target, koalaIRS12, links Reed-Solomon proximity research to the security assumptions behind hash-based SNARKs used across zero-knowledge systems.The most meaningful feature is the workflow: solvers may use AI agents, but the accepted output must be a Lean-checked proof that improves the soundness bound. If the model works, it could give the Ethereum research ecosystem a repeatable way to convert agent-assisted exploration into auditable formal evidence.
The launch should not be read as a market signal or as proof that the 128-bit target has already been reached. It is a public research mechanism for closing the gap between conjectured and proven security, one accepted proof artifact at a time.
Sources
Editorial Team - CoinBotLab
