以太坊研究論壇發布以太坊 TCB 客戶端文章

以太坊基金會成員 George Kadianakis 和 Kev Wedderburn 在以太坊研究論壇發布了「以太坊 TCB，第一部分：客戶端」文章。文章定義了可信計算基（TCB）為被信任而非被證明的組件、規範、工具與假設，並探討在形式化驗證普及後，抽象以太坊客戶端的 TCB 如何縮小。文章主張將軟體拆分為易驗證的「純」模組（如密碼學、SSZ）與帶副作用、難驗證的「髒」模組（如網路），將髒模組視為不可信，集中驗證純模組，並儘量將已驗證邊界推到網路解析、gossip 與同步邏輯。文章還區分了「用 Lean4 寫規範並證明性質」與「證明實現符合該規範」。具體路徑包括將 Rust 等實現翻譯到 Lean4（翻譯器與 Rust 編譯器仍進入 TCB），在 Lean4 中編寫模組並抽取為 C，客戶端儘量用 Lean4 編寫，使用 RISC-V 彙編繞開常規編譯器（ISA 模型等仍進入 TCB），或使用已驗證編譯器。