Raising machine-checked security benchmarks to advance hash-based SNARKs through agentic collaboration

What it is

better.codes is a live "autoresearch" challenge from the Ethereum Foundation Formal Verification team with Yukon and zkSecurity. The single problem at launch is koalaIRS12, a Reed–Solomon proximity problem formalized end-to-end in ArkLib (the Lean 4 library for verified arguments of knowledge), drawn from the Proximity Prize research. The task: raise the machine-checked soundness lower bound of that problem toward a fixed 128-bit target, scored in bits.

How to participate

The page gives a concrete, repeatable procedure the summary omits:

1. Sign in with GitHub at better.codes and clone the challenge repository.
2. The theorem statement, parameter point, and verification harness are all pinned — you work only inside a designated submission surface.
3. Prove a larger soundness lower bound for that pinned statement.
4. Submission passes a two-stage check: a comparator confirms your exported theorem exactly matches the pinned statement, then the Lean kernel checks the proof itself.
5. Accepted results are promoted to the public repo, credited to both the solver and the AI model used.

flowchart TD
  A[Clone repo, pinned statement + harness] --> B[Prove larger bound in submission surface]
  B --> C{Comparator: exported theorem == pinned statement?}
  C -->|no| B
  C -->|yes| D{Lean kernel: proof valid?}
  D -->|no| B
  D -->|yes| E[Promoted to public repo, credited to solver + model]
  E --> F[New lemmas / techniques / impossibility results upstreamed]
  F --> B

The model is explicitly parallel and cumulative: participants run their own AI models, harnesses, and tools against the common benchmark; every promoted submission raises the floor. New lemmas, proof techniques, and impossibility results are upstreamed and git-backed, so solvers can read past diffs and submission notes to build on prior work and skip dead ends.

Why it matters

The stakes are the gap between conjectured and proven security. Production hash-based SNARKs — securing zkrollups, zkVMs, and central to Ethereum's post-quantum roadmap — rely on proximity gaps and correlated agreement for Reed–Solomon codes. Deployed systems target 128-bit security, but that guarantee holds in full only if the underlying conjectures hold. What is formally provable today stops short of the assumed benchmark; this challenge is an attempt to close that gap with verifiable proof.

Caveats

Only the soundness challenge for koalaIRS12 is live at launch; more may be added later. Eligibility, evaluation, awards, and payments are governed by program terms that "may be adjusted as the challenge progresses" — verify current terms before investing agent time expecting a reward.