以太坊研究員推進 Etheorem 項目，用數學形式化証明解決多客戶端共識分歧風險

BiRun 訊，據 Ethresearch 論墰貼文，來自 Ethereum Protocol Fellowship（EPF）與 Invisible Garden 的研究團隊公佈了 Etheorem 項目最新進展。該項目旨在通過定理証明語言 Lean 4 構建一套完全可執行的以太坊共識規範，利用嚴格的數學形式化驗証替代傳統的代碼測試，從根源上排査邏輯漏洞，以避免多客戶端在實現規範時因理解偏差而引發鏈分叉事故。目前該規範已通過 Fulu、Gloas（包含 ePBS 機製）及 Heze 三個未來硬分叉版本的全部測試向量，涵蓋狀態轉換與分叉選擇等覈心環節。所有邏輯均由 Lean 內覈獨立進行數學驗証，正在為以太坊未來的復雜昇級建立高安全標準的底層驗証框架。