新聞 
幣種資訊 
關於我們 
以太坊（Ethereum）研究團隊正以 Lean 4 實作並從數學上驗證 Fulu、Gloas 與 Heze 升級的共識規格，盼降低不同客戶端對同一規格產生不同解讀、進而導致鏈分裂的風險。
以太坊協議獎學金（Ethereum Protocol Fellowship，EPF）與 Invisible Garden 研究團隊21日在以太坊研究論壇（Ethereum Research Forum）貼文公開「Etheorem」專案進展。Etheorem 旨在利用定理證明語言 Lean 4，將以太坊共識規格實作成可執行形式，並超越程式碼測試，從數學上驗證核心邏輯。
以太坊採用多個開發團隊共同維護的共識客戶端架構。即使各客戶端實作相同規格，只要對細部邏輯的理解不同，仍可能導致區塊有效性判斷或鏈選擇結果出現差異。Etheorem則透過形式驗證檢查這類解讀差異。
專案已實作對應 Fulu、Gloas 與 Heze 升級的共識規格，並能執行狀態轉換與分叉選擇邏輯。目前團隊正將實作結果與以太坊官方共識測試向量比對，以確認其正確性。Fulu包含資料可用性抽樣相關規格；Gloas則納入執行層酬載拍賣結構 ePBS；Heze則反映旨在抗審查的納入清單結構。
Etheorem 的基礎是 SSZ（Simple Serialize）函式庫 SizzLean。該函式庫在 Lean 核心中驗證共識資料序列化、反序列化及默克爾樹計算所需的部分屬性。驗證項目包括序列化資料能否還原為原始值、不同值是否不會使用相同編碼，以及編碼大小是否超過預先計算的限制。
專案也著重縮小經過驗證的程式碼與實際執行程式碼之間的差距。團隊計畫在驗證環境與執行環境中共同使用同一套規格定義，以降低用於證明的邏輯與實際客戶端邏輯不一致的問題。由於形式驗證只能檢查適用範圍內的邏輯，這並不代表 Etheorem 已進入取代完整以太坊客戶端的階段。TokenPost先前報導的區塊鏈協議 Lean 4 形式驗證案例，同樣是先以模型重現核心邏輯，再設定驗證範圍。
通過測試向量也不代表營運環境已獲得穩定性保證，或專案已正式發布。團隊表示，未來將擴大證明涵蓋的範圍。
留言 0