Foresight News 消息，以太坊基金会成员 George Kadianakis 和 Kev Wedderburn 于以太坊研究论坛发布「以太坊 TCB，第一部分：客户端」文章。文中将可信计算基（TCB）定义为被信任而非被证明的组件、规范、工具与假设，并讨论在形式化验证普及后，抽象以太坊客户端的 TCB 会如何缩小。文章主张把软件拆成易验证的「纯」模块（如密码学、SSZ）与带副作用、难验证的「脏」模块（如网络）：把脏模块视为不可信，集中验证纯模块，再将已验证边界尽量推到网络解析、gossip 与同步逻辑。

落地上，文章区分「用 Lean4 写规范并证明性质」与「证明实现符合该规范」。具体路径包括：将 Rust 等实现翻译到 Lean4（翻译器与 Rust 编译器仍进入 TCB）；在 Lean4 中编写模块并抽取为 C；客户端尽量用 Lean4 编写；用 RISC-V 汇编绕开常规编译器（ISA 模型等仍进入 TCB）；或使用已验证编译器。