better.codes

Direct answerbetter.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 problemFRI / STIR / WHIR soundnessLean 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 (2026-09-13): Active (launched 2026-08-20)
First public release: 2026-08-20

Last reviewed 2026-09-13 by the sorryfree editors.

What better.codes does

Every submission is checked by the Lean kernel; promoted proofs are upstreamed and credited to the solver and the model used. The attack (upper) bound on the same problem is 116.13 bits, so the gap between what is proven and what is believed is the object of the challenge.

The Proximity Prize is a $1M Ethereum Foundation research fund for list-decoding and correlated-agreement bounds for Reed-Solomon codes; Yukon is an autoresearch platform operated by Eigen Labs. better.codes matters to this index because it is the first public venue where AI-driven proving on a cryptographic bound is measured with a kernel rather than a leaderboard of claims.

Where it is strong

Machine-checked progress on a bound that decides real SNARK security levels.
Public, dated, attributed results.
Demonstrates AI-assisted proving under kernel discipline.

Limits and caveats

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.

When to choose it

Follow better.codes if your security argument depends on FRI, STIR or WHIR soundness, or if you want to see how AI provers perform on real cryptography.

Who works with better.codes

zkSecurity.

Top-listed for verified-circuit work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website

zk.golf, Verified zkEVM program.

Sources

Last reviewed 2026-09-13 by the sorryfree editors. Machine-readable: data.json · summary.txt