Formal verification does not remove trust from a client, it shrinks it
Serguey Asael Shinder2 min readGeorge and Kev have posted the first part of an analysis of Ethereum's Trusted Computing Base on ethresear.ch, with thanks to Alex Hicks. The framing is the useful part. Their motivation is blunt - "it's 2026 and AI has been breaking the Internet lately", and formal verification looks like the defender's long-run edge - but they immediately refuse the easy version of that claim.
The lens they propose is the TCB: every component, specification, tool and assumption that is trusted rather than proven, which is precisely what humans must still check. Formal verification, they state plainly, cannot remove the TCB entirely - it can significantly shrink it. So the question worth asking is not whether a client is verified but what its TCB looks like afterwards.
Scope is deliberately narrowed: not the Ethereum protocol, which they call vast and complicated, but an abstract Ethereum client. Two themes carry the post - how to split software into modules that can be formally verified, and how to achieve end-to-end verification rather than a collection of verified pieces. Their prover is Lean4, which they describe as a sign of the times rather than a requirement: the argument holds with any proof assistant.
What it means
"Formally verified" is on its way to becoming the kind of label that stops carrying information, and the TCB framing is the antidote. A proof is always relative to a specification, a compiler, a runtime and a set of assumptions, and if the specification is wrong the proof is a guarantee that the code faithfully implements the mistake. Asking what remains trusted converts a marketing adjective into a list - and a list can be reviewed, argued over, and shortened deliberately.
The end-to-end theme is where the real difficulty sits, and it is a familiar failure in ordinary engineering too. Verifying modules individually and then composing them leaves the interfaces unproven, which is exactly where the interesting bugs live; a set of green module proofs can coexist with a broken system. That is the same structural point as a security control whose visible half is installed and whose deciding half never runs - the parts pass and the whole does not.
For anyone reading client-security claims, the practical question this post hands you is short: what is in the TCB, and who checked it? A client team that can answer with a specific list - this specification, this compiler, these assumptions about the execution environment - is doing verification. One that answers "we use Lean4" is naming a tool. Part 2 will presumably widen this from the client to the protocol, which is where the assumptions get genuinely hard.