better.codes: the Proximity Prize soundness challenge with Lean 4 checked submissions
================================================================================

better.codes is an open autoresearch challenge built by the Ethereum Foundation Formal Verification team with Yukon and zkSecurity. A self-contained problem from the Proximity Prize (koalaIRS12, a Reed-Solomon proximity question that governs the provable soundness of hash-based SNARKs such as FRI, STIR and WHIR) is formalised in Lean 4, and solvers direct AI agents at raising the proven soundness lower bound. As of 2026-09-13 the bound stood at 68.07 bits against a 128-bit target, up from a 64-bit literature baseline, with 74 promoted submissions from 22 solvers.

Maintainer: Ethereum Foundation Formal Verification team, Yukon and zkSecurity
Website: https://better.codes
Category: Challenges and programs
Targets: koalaIRS12 proximity problem, FRI / STIR / WHIR soundness, Lean 4
Approach: A formalised open problem from the Proximity Prize; solvers point AI agents at improving the machine-checked lower bound; every submission is kernel-checked and promoted proofs are credited
Access: Open challenge; program terms on the site
Status: Active (launched 2026-08-20)
Strengths: Machine-checked progress on a bound that decides real SNARK security levels. | Public, dated, attributed results. | Demonstrates AI-assisted proving under kernel discipline.
Limits: A single problem, not a general tool. | Requires Lean 4 and proximity-testing expertise to contribute meaningfully. | Bound remains far from the 128-bit target.
Firms using it: zkSecurity
Sources: https://better.codes | https://blog.ethereum.org/en/2026/08/20/better-codes-challenge | https://proximityprize.org | https://www.yukon.org

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