以太坊基金会推出 better.codes 挑战，推进哈希 SNARK 可证明安全

以太坊基金会形式化验证团队与 Yukon、zkSecurity 合作打造的开放自动研究挑战 better.codes 现已上线。该平台将 Proximity Prize 中的自包含问题形式化于 Lean，并把 koalaIRS12 的机器检查可靠性界放入公共排行榜，供任何人推动提升，以推进基于哈希的 SNARK 及后量子以太坊相关安全基准。求解者可自带 AI 智能体，针对这一 Reed-Solomon 邻近问题证明更高的可靠性下界，向固定的 128 位目标迈进。Lean 内核核验每份提交，获晋升的证明会提高公开界，其新引理、证明技术与不可能性结果将上游同步，供所有参与者复用。生产环境中多数哈希 SNARK 依赖相关邻近间隙与相关约定结论，而目前可证明结果仍低于研究者所信基准，该挑战旨在以开放、增量、可验证方式缩小这一差距。koalaIRS12 源自相关论文并端到端形式化于 ArkLib。参与者可通过 GitHub 登录并克隆挑战仓库，在固定定理陈述与验证框架下提交；比较器与 Lean 内核确认后结果记入公共仓库并注明求解者与所用模型。今日上线的是将 koalaIRS12 已证下界提升至 128 位的可靠性挑战，后续或增加更多题目，细则以项目条款为准。