better.codes 是什么，如何参与？以太坊基金会 SNARK 可靠性挑战说明

以太坊基金会形式化验证团队与 Yukon、zkSecurity 合作创建的开放自动化研究挑战平台 better.codes 已正式上线。该平台将 Proximity Prize 中的自包含问题使用 Lean 进行形式化，并把 koalaIRS12 的机器检验可靠性边界置于公共排行榜上，允许任何人参与改进，以推进基于哈希的 SNARK 及后量子以太坊相关安全基准。

求解者可以自带 AI 代理，针对该 Reed-Solomon 邻近性问题证明更高的可靠性下界，朝着 128 位的固定目标推进。Lean 内核将对每次提交进行验证，被采纳的证明将提升公共边界；新的引理、证明技术及不可能性结果也会同步至上游，供所有参与者复用。当前生产环境中的大多数哈希 SNARK 依赖相关邻近间隙与一致性结论，但可证明的结果仍低于研究人员所信任的基准，本次挑战旨在以开放、增量且可验证的方式缩小这一差距。

koalaIRS12 源自相关论文，并已在 ArkLib 中完成端到端形式化。参与者可通过 GitHub 登录并克隆挑战仓库，在固定的定理陈述与验证框架下提交；经比较器与 Lean 内核确认的结果将记录于公共仓库，并注明求解者及其使用的模型。本次发布聚焦将 koalaIRS12 已证明下界提升至 128 位的可靠性挑战，后续可能在项目条款约束下增加更多问题。

挑战核心要点

• 主导方：以太坊基金会形式化验证团队，联合 Yukon、zkSecurity 共建。 • 当前挑战对象：koalaIRS12 的 Reed-Solomon 邻近性问题。 • 验证方式：Lean 内核机器检验，确保提交证明的公开可验证性。 • 目标：将可靠性下界提升至 128 位。 • 社区共享：所有新引理、证明技术与不可能性结果将同步上游，供后续复用。

如何参与提交

参与者需使用 GitHub 账号登录 better.codes，克隆公开的挑战仓库，并在预先设定的定理陈述与验证框架内完成提交。系统通过比较器与 Lean 内核对结果进行双重确认，验证通过后将自动写入公共仓库，同时记录求解者身份及所使用的 AI 模型。

技术背景与后续观察

生产级哈希 SNARK 方案普遍依赖邻近间隙与相关一致性结论，但目前学术界可证明的可靠性边界仍低于工程实践的信任阈值。better.codes 通过公共排行榜与自动化机器验证，试图以可复现的方式逐步缩小这一差距。由于 koalaIRS12 已在 ArkLib 中完成端到端形式化，参与者提交的有效证明将直接提升公共可靠性边界。后续可关注该平台是否扩展更多问题集，以及 128 位目标达成后的实际安全基准变化。