以太坊研究論墰發布「以太坊 TCB，第一部分：客戶端」文章

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