The Ethereum Foundation has launched better.codes, a novel competitive research initiative designed to accelerate the formal verification of zero-knowledge proof systems. Developed by the Foundation's Formal Verification team alongside Yukon and zkSecurity, the platform transforms a historically isolated academic pursuit into a crowdsourced optimization challenge accessible to the broader cryptography community. At its core sits a rigorously formalized mathematical problem—lifted directly from the Proximity Prize research agenda—expressed in Lean, a proof assistant language that enables machine-checked correctness guarantees.
The mechanism is straightforward but elegant: better.codes presents a concrete soundness bound derived from hash-based SNARK constructions and publishes it on a public leaderboard where researchers can iteratively improve upon previous results. Rather than waiting for peer review cycles or siloed academic collaboration, the platform creates real-time competitive pressure to tighten security parameters. This approach acknowledges a fundamental reality in applied cryptography: theoretical bounds often contain considerable slack, and incremental improvements in provable security can translate directly into reduced computation overhead or smaller proof sizes in production systems. By formalizing the problem statement in Lean, all contributions remain machine-verifiable, eliminating ambiguity about claim validity.
Hash-based SNARKs represent a critical research direction for post-quantum cryptography resilience, as they rely on collision-resistant hash functions rather than elliptic curve assumptions vulnerable to quantum algorithms. However, these constructions typically carry larger proof sizes and computational costs than their discrete-log counterparts, making efficiency improvements particularly valuable. The better.codes leaderboard essentially invites the global cryptography community to collectively debug and optimize these security proofs, treating formal verification as an iterative, gamified process rather than a one-time gate.
This initiative reflects a broader shift within the Ethereum ecosystem toward treating cryptographic soundness not as a solved problem but as a continuously improvable parameter. By combining formal verification rigor with community incentives, better.codes demonstrates that even highly theoretical research can benefit from transparent, competitive collaboration. As zero-knowledge technologies mature beyond experimental stages into production infrastructure, tightening these bounds could meaningfully reduce computational friction across privacy-preserving and scaling solutions.