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