Foresight News|Sep 25, 2026 12:02
[Ethereum Research Forum Publishes 'Ethereum TCB, Part 1: Clients' Article]
Foresight News reports that Ethereum Foundation members George Kadianakis and Kev Wedderburn have published an article titled 'Ethereum TCB, Part 1: Clients' on the Ethereum Research Forum. The article defines the Trusted Computing Base (TCB) as components, specifications, tools, and assumptions that are trusted rather than proven, and discusses how the TCB of an abstract Ethereum client could be reduced with the widespread adoption of formal verification. The article advocates splitting software into easily verifiable 'pure' modules (e.g., cryptography, SSZ) and 'dirty' modules with side effects that are harder to verify (e.g., networking): treating dirty modules as untrusted, focusing verification on pure modules, and pushing the verified boundaries as far as possible to network parsing, gossip, and synchronization logic.
In terms of implementation, the article distinguishes between 'writing specifications in Lean4 and proving their properties' and 'proving implementations conform to those specifications.' Specific approaches include: translating Rust implementations into Lean4 (with the translator and Rust compiler still part of the TCB); writing modules in Lean4 and extracting them to C; writing clients primarily in Lean4; bypassing conventional compilers using RISC-V assembly (with ISA models still part of the TCB); or using verified compilers.
Share To
Timeline
HotFlash
APP
X
Telegram
CopyLink