以太坊基金會推出 better.codes 挑戰，推進哈希 SNARK 可證明安全

以太坊基金會形式化驗證團隊與 Yukon、zkSecurity 合作打造的開放自動研究挑戰 better.codes 現已上線。該平臺將 Proximity Prize 中的自包含問題形式化於 Lean，並把 koalaIRS12 的機器檢查可靠性界放入公共排行榜，供任何人推動提升，以推進基於哈希的 SNARK 及後量子以太坊相關安全基準。求解者可自帶 AI 智能體，針對這一 Reed-Solomon 鄰近問題證明更高的可靠性下界，向固定的 128 位目標邁進。Lean 內核核驗每份提交，獲晉升的證明會提高公開界，其新引理、證明技術與不可能性結果將上游同步，供所有參與者複用。生產環境中多數哈希 SNARK 依賴相關鄰近間隙與相關約定結論，而目前可證明結果仍低於研究者所信基準，該挑戰旨在以開放、增量、可驗證方式縮小這一差距。koalaIRS12 源自相關論文並端到端形式化於 ArkLib。參與者可通過 GitHub 登入並克隆挑戰倉庫，在固定定理陳述與驗證框架下提交；比較器與 Lean 內核確認後結果記入公共倉庫並註明求解者與所用模型。今日上線的是將 koalaIRS12 已證下界提升至 128 位的可靠性挑戰，後續或增加更多題目，細則以項目條款為準。