Ethereum researchers race to close zkEVM security gap before December target
Key Takeaways
- •The Aug. 21 leaderboard for koalaIRS12 showed a 63.99-bit lower certificate and a 116.13-bit upper certificate, leaving 52.14 bits unresolved after nine promoted submissions from seven solvers.
- •The contest runs two opposing tracks in which soundness submissions raise the lower certificate and attack submissions lower the upper certificate, with every promoted proof verified by the Lean kernel in a pinned environment.
- •The Ethereum Foundation's zkEVM roadmap calls for 128-bit provable security, final proofs of 300 KiB or less, and a formal soundness argument for the recursion architecture, with the M3 deadline moved to early December 2026.
- •The challenge score applies only to the encoded parameter point and is expressly not a measure of whole-system soundness or full-protocol security, which would require separate analysis.
- •The contest's immediate impact is confined to research evidence, because zkEVM execution proofs currently supplement mainnet testing in a non-consensus-critical phase without changing Ethereum's validation path.

Ethereum researchers race to close zkEVM security gap before December target
Ethereum's better.codes contest has turned a cryptographic proof gap into a public, reproducible measurement that researchers can push from both sides.
At 15:44:47 UTC on Aug. 21, the live leaderboard showed a 63.99-bit lower certificate and a 116.13-bit upper certificate for koalaIRS12. After nine promoted submissions from seven solvers, 52.14 bits remain unresolved between the two bounds.
KoalaIRS12 is a fixed parameter profile for an interleaved Reed–Solomon reduction used in proof-system research. Reed–Solomon proximity questions of this kind are foundational rather than peripheral: FRI, the Fast Reed–Solomon IOP of Proximity, is the technique that STARKs and other hash-based SNARKs use to test whether a committed string lies close to a low-degree polynomial. The challenge repository defines its score as a spot-check quantity and expressly excludes interpreting it as minus-log2 of whole-system soundness or as full-protocol security. What researchers now hold is a public measure of the distance between what the challenge has proved safe and what its upper certificate still rules unsafe.
What the leaderboard proves
The contest runs two tracks designed to close the interval from opposite directions.
The soundness track raises the lower certificate. At a certified radius, a successful submission proves that the benchmark's executable reduction-error bound meets the encoded target, then maps that radius to the score displayed on the board.
The attack track lowers the upper certificate. Its theorem certifies an unsafe suffix under the benchmark's winning-set-density condition, and the repository covers that suffix directly because the formalization assumes no monotonicity theorem for winning-set density. The upper-certificate track's score describes the formal boundary for koalaIRS12; an Ethereum attack cost would require a separate whole-system analysis.
According to the Ethereum Foundation's launch announcement, the theorem statement, parameter point, and verification harness are pinned. Each submission exports the required theorem, a comparator checks that statement against the target, and the Lean kernel verifies the proof before promotion. Lean is an interactive theorem prover whose small trusted kernel machine-checks every proof step. An accepted result proves the submitted theorem inside that pinned environment.
Production assurance reaches further than that. It must also cover the model's completeness, the assumptions embedded in its definitions, implementation fidelity, and the composition of separately analyzed components. The Foundation's May review of a formal-verification effort on SP1, a zkVM developed by Succinct, shows why those additional layers matter: specifications and theorem statements are code, inputs and versions need reproducible pinning, and component-level results require broader reasoning before they can support conclusions about a full system.
A separate academic paper by Gal Arnon, Dan Boneh and Giacomo Fenzi identifies list decoding, Reed–Solomon proximity gaps, correlated agreement and mutual correlated agreement as open questions for succinct proof systems. Published before the current leaderboard snapshot, it explains the importance of the problem family without evaluating today's scores.
The Foundation frames better.codes as a machine-checked research path for hash-based SNARK security, and improving the koalaIRS12 certificates would sharpen one reduction within that agenda. The 116.13-bit certificate has the same limited reach: it applies to the parameter point encoded in the challenge, while other parameter choices, constructions, and system components remain separate research questions.
The two-sided format is what makes the interval informative. Every promotion changes a checkable boundary, and the pinned theorem keeps successive results comparable.
The gap to Ethereum's December target
The Foundation's December 2025 zkEVM security roadmap called for 128-bit provable security — a bar conventionally read as an attack requiring on the order of 2^128 operations — along with a final proof size of 300 KiB or less and a formal soundness argument for the recursion architecture. A February security-sprint update moved the M3 deadline to early December 2026 and aligned the architecture-security argument with a Dec. 1 deliverable. The roadmap asks teams to connect component bounds to an auditable system package.
For koalaIRS12, a lower certificate reaching the encoded 128-bit target would settle the soundness side of the benchmark at its fixed parameter point. A production zkEVM claim would additionally need soundness accounting across every relevant component, proof-size compliance, a documented recursion topology, an argument for how its parts compose, and evidence that specifications match implementations.
The Foundation's public progress page, last synced Aug. 20, lists zkVM readiness and ISA compliance results and names real-time proving and soundcalc integration as criteria. Its rendered tables contain no completion marker for the full early-December package and remain silent on work tracked elsewhere.
A May update on optional execution proofs described a non-consensus-critical phase in which zkEVM proofs supplement mainnet testing while ordinary execution-client re-execution continues to drive attestation. That optional role keeps the leaderboard's immediate consequence in the research domain: movement in the certificates changes the evidence available for future security arguments without changing Ethereum's current consensus-critical validation path.
On better.codes, soundness submissions can lift the 63.99-bit lower certificate and attack submissions can pull the 116.13-bit upper certificate down. Across the zkEVM roadmap, teams must publish the system-level accounting, proof sizes, recursion arguments, and implementation evidence required for the early-December review.
For now, the 52.14-bit interval stands as a live measure of unfinished work on koalaIRS12. Ethereum's 128-bit production case will depend on how that component evidence fits into the larger proof.
Source: CryptoNews