以太坊研究论坛发布客户端可信计算基文章

据 Woofun AI 消息，基金会成员 和 在以太坊研究论坛发布题为"以太坊 TCB，第一部分：客户端"的文章。文中将可信计算基（TCB）界定为被信任而非被证明的组件、规范、工具与假设，并分析在形式化验证普及后，抽象以太坊客户端的 TCB 范围如何缩小。

文章主张将软件拆分为易验证的"纯"模块（如密码学、SSZ）与带副作用、难验证的"脏"模块（如网络），视脏模块为不可信，集中验证纯模块，并将已验证边界延伸至网络解析、gossip 与同步逻辑。落地路径包括区分"用 Lean4 写规范并证明性质"与"证明实现符合该规范"，具体涵盖将 Rust 等实现翻译到 Lean4、在 Lean4 中编写模块并抽取为 C、客户端尽量用 Lean4 编写、用 RISC-V 汇编绕开常规编译器，或使用已验证编译器。