better.codes

The open automated research challenge better.codes, created by the Ethereum Foundation's formal verification team in collaboration with Yukon and zkSecurity, is now live. This platform formalizes the self-contained problems from the Proximity Prize in Lean and places the machine-checked reliability bounds of koalaIRS12 on a public leaderboard, allowing anyone to contribute to improvements, advancing hash-based SNARK and post-quantum Ethereum-related security benchmarks.Solvers can bring their own AI agents to prove higher lower bounds of reliability for this Reed-Solomon proximity problem, moving towards a fixed target of 128 bits. The Lean kernel verifies each submission, and the promoted proofs will enhance the public bounds, with new lemmas, proof techniques, and impossibility results being synchronized upstream for reuse by all participants. Most hash SNARKs in production environments rely on related proximity gaps and related conclusion agreements, while the currently provable results remain below the benchmarks trusted by researchers; this challenge aims to narrow this gap in an open, incremental, and verifiable manner.koalaIRS12 originates from related papers 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; results confirmed by the comparator and Lean kernel are recorded in a public repository, noting the solver and the model used. Today's launch features the reliability challenge that raises the proven lower bound of koalaIRS12 to 128 bits, with more problems potentially added later, subject to project terms.