Ethereum Foundation Launches better.codes Challenge to Advance Hash-Based SNARK Provable Security

The Ethereum Foundation's formal verification team, in collaboration with Yukon and zkSecurity, has launched better.codes, an open automated research challenge now live. The platform formalizes self-contained problems from the Proximity Prize in Lean and places machine-checked reliability bounds for koalaIRS12 on a public leaderboard, open for anyone to improve, advancing security benchmarks for hash-based SNARKs and post-quantum Ethereum. Solvers can bring their own AI agents to prove higher reliability lower bounds for this Reed-Solomon proximity problem, moving toward a fixed 128-bit target. The Lean kernel verifies each submission, and promoted proofs raise the public bound, with new lemmas, proof techniques, and impossibility results synced upstream for all participants to reuse. Most hash-based SNARKs in production rely on related proximity gaps and related agreement conclusions, yet current provable results remain below benchmarks researchers believe, and this challenge aims to close that gap in an open, incremental, and verifiable manner. koalaIRS12 originates from a related paper and is end-to-end formalized in ArkLib. Participants can log in via GitHub and clone the challenge repository, submitting under fixed theorem statements and verification frameworks; after confirmation by the comparator and Lean kernel, results are recorded in the public repository with the solver and model noted. Launched today is the reliability challenge to raise koalaIRS12's proven lower bound to 128 bits, with more problems potentially added later, subject to project terms.