イーサリアム・ファウンデーションのメンバーであるジョージ・カディアナキスとケヴ・ウェダーバーンは、Ethereum Research Forum上で「Ethereum TCB, Part One: Clients」という題名の論文を公開した。Foresight Newsによると、この記事は信頼された計算基盤（TCB）を、「実証されるのではなく、信頼される」コンポーネント、仕様、ツール、仮定として定義しており、形式検証がより一般的になるにつれて、イーサリアム・クライアントのTCBがどのように縮小し得るかを論じている。

この記事は、暗号やSSZのような、検証しやすい「純粋な（pure）」モジュールと、ネットワーキングのように副作用を伴い検証しにくい「汚れた（dirty）」モジュールにソフトウェアを分割することを主張している。汚れたモジュールは信頼できないものとして扱うべきであり、検証は純粋なモジュールに集中し、検証済みの境界を可能な限りネットワーク解析、ゴシップ、同期ロジックへ押し広げるべきだとしている。

この記事は、Lean4において仕様を書くことと性質を証明することを区別し、さらに実装が仕様に一致することを証明することについても述べています。いくつかのアプローチを概説しており、その例として、Rustの実装をLean4に翻訳する方法があります（このとき翻訳器とRustコンパイラはいずれもTCBに含まれたままです）。また、Lean4でモジュールを書いてそれをCに抽出する方法、Lean4上でクライアントを直接構築する方法、通常のコンパイラを迂回するためにRISC-Vアセンブリを用いる方法（ただしISAモデルはTCBに含まれたままです）、あるいは検証済みコンパイラを用いる方法などがあります。