以太坊的 TCB（第一部分）：客户端

以太坊研究文章探讨在形式化验证（FV）视角下，一个抽象以太坊客户端的可信计算基（TCB）应如何划分与缩小。文章提出将客户端拆分为易验证的纯模块（如密码学、SSZ、分叉选择规则）与难以验证的脏模块（如网络模块），并给出端到端 FV 的四种路径，包括 Rust 到 Lean4 的翻译器、用 Lean4 编写模块、Lean-maxxing 等方案。