Ethereum Research 提案探讨以太坊客户端的形式化验证与 TCB

George 和 Kev 在 Ethereum Research 发文，以 TCB（可信计算基）为视角分析抽象以太坊客户端的形式化验证，将客户端模块分为易验证的纯模块和难验证的脏模块，并提出先将脏模块建模为不可信、再逐步向外扩展验证边界的两步做法。