以太坊基金会推出了 Better Codes，这是一项开放式自动研究挑战赛，重点是提高 koalaIRS12 的机器验证健全性界限。koalaIRS12 是一个与基于哈希的 SNARK 相关的 Reed–Solomon 邻近性问题。参赛者可以使用 AI 智能体、模型、提示词和自动化测试工具，但提交内容必须经过 Lean 4 内核验证。该挑战赛旨在缩小生产系统所针对的128位安全性，与底层邻近性猜想及相关一致性猜想已被形式化证明的程度之间的差距。获奖者将共同分享以太坊基金会100万美元的 Proximity Prize 奖池。该项目由以太坊基金会形式化验证团队与 Yukon 和 zkSecurity 共同打造；较新的账户还将 Eigen Labs 列为联合构建方。该项目已在 ArkLib 中完成形式化。ArkLib 是一个用于形式化验证知识论证的 Lean 4 库。