Thanks to Alex Hicks for the many stimulating discussions that shaped this post.
Motivation
It’s 2026 and AI has been breaking the Internet lately. Formal verification (FV) seems to be the way for defenders to get an edge in the long run.
However, formal verification is a term that’s thrown around easily and it’s worth digging deeper to see what it means in the context of Ethereum.
An important lens when thinking about formal verification is the TCB (Trusted Computing Base): every component, spec, tool and assumption that is trusted rather than proven. That is what humans must still check. Formal verification cannot remove the TCB entirely, but it can significantly shrink it.
It’s hence worth asking:
“How does Ethereum’s TCB look like in a post-FV world?”
Overview
The Ethereum protocol is vast and complicated and while analyzing its TCB is worthwhile, in this post we will restrict ourselves to an easier problem and discuss the TCB of an abstract Ethereum client.
In this post, we discuss two main themes:
- how to split software into modules that get formally verified
- how to achieve end-to-end formal verification
Our theorem prover is Lean4, a sign of the times rather than a requirement. Everything below works with any proof assistant.
Ethereum clients and FV
Looking at an Ethereum client from the lenses of formal verification, we first need to decide what the client as a whole should guarantee (e.g. it never signs two conflicting attestations).
We then break the client into modules, fix the interfaces between them, and work out which guarantee each module should carry. The whole-client guarantee follows from the module guarantees, composed along those interfaces.
In general, some modules are easy to formally verify, whereas others are hard or impossible:
- Pure modules are easy to FV: they have zero or minimal side effects, are mathy, and have clean interfaces. For example cryptography, SSZ, or fork choice rules.
- Dirty modules are hard to FV: they are full of side effects and I/O. For example modelling a networking module is messy, since messages might arrive out-of-order, connections might drop, messages might arrive too late, etc.
Handling dirty modules
There will be lots of dirty modules in an Ethereum client (possibly more than half of the total volume), so handling them well matters. The way to do it is in two steps:
The first step is to carefully model dirty modules as untrusted-by-design.
For example, consider a dirty networking module that passes signatures to a pure signature verification module. With the right threat model, every output of the networking module is treated as untrusted: this becomes an explicit assumption of the signature module’s formal model, so its theorems hold for any input. A bug in the networking module then looks no different from a hostile peer, and the proof already covers it.
The second longer-term step is to push the verified boundary outwards and FV the dirty modules too, as close to the wire as possible. Modelling and verifying the network is hard, but by verifying the parsers, gossip rules and sync logic that sit on top of it, we can prove that no message can crash them or make them eat unbounded resources.
From a spec to the binary
Ethereum users don’t care about Lean4 theorems and specs. They only care that the code that runs on their computers is secure.
So what really matters is end-to-end FV: the proofs must reach as close to the binary a user actually runs as possible.
Let’s split the task of end-to-end FV into two halves:
- writing a formal spec in Lean4 and proving theorems about it
- and proving that an implementation matches the Lean4 spec
Take an SSZ module as an example. The first half is writing its spec and proving, say, that decoding gives back the original value. The second half is showing that the SSZ code inside a client does what that spec says.
Writing good specs is hard. However, in this post, we take some artistic freedom and take the spec as given, so that we can focus our attention on the second half of the problem.
Verifying end-to-end
There have been many proposals for end-to-end FV (see this survey and this talk). They all share a common theme:
You somehow prove that the source code corresponds to the formal model proven in Lean4, and also try to prove the correctness of whatever turns that source code into the binary.
Of course that’s not trivial, because the source code side is written in Rust/Go/C#, whereas the model side is Lean4. Linking these two worlds is hard, and there are a bunch of suggested approaches to do so.
Consider a client written in Rust (the same holds for Go, C#, etc). We look at four options for end-to-end FV:
Option 1: Translator
In this approach, modules stay in Rust and get auto-translated to Lean4 using some translator software.
Big companies like Microsoft have poured millions of dollars into developing tools for this approach. For example, Aeneas is exactly that for Rust-to-Lean, and hax is a similar tool.
This approach suffers from two issues: The translator itself is part of the TCB. Also languages like Rust don’t have formal semantics, so the translator can only handle a subset of the language, and the client code has to stay inside that subset. This last issue is particularly limiting (see sproul’s attempt with Aeneas).
Worth mentioning that in this approach, the Rust compiler that prepares the final binary is also part of the TCB.
Option 2: Modules written in Lean4
In this approach, we write modules in Lean4 itself, so the proofs talk about the implementation itself. The code is then extracted to C and integrated with the client using bindings.
What stays trusted is the Lean-to-C extractor (leanc), the C compiler and the FFI bindings.
Option 3: Lean-maxxing
In this approach, the client itself is written in Lean4 and compiled the same way as the option above.
Dirty modules stay in whatever language fits and are FFI’d in. Same TCB as option 2: extractor, C compiler, bindings.
The positive aspect of this option is that it allows the proofs to reach deeper into the glue between the modules.
Option 4: Assembly
In this approach, modules are written directly in RISC-V assembly. This seems insane at first, but it allows us to completely remove the compiler from the TCB.
The Lean spec and the assembly are connected by a formal model of the RISC-V ISA, and that model is trusted. AWS is using this option for bignum arithmetic in production via the s2n-bignum library. We also need an emulator, or a translator, that takes us from RISC-V assembly to x86 or ARM assembly depending on the machine that the user has.
Option 5: Verified compiler
In this approach, modules are written in an FV-friendly language whose compiler has been proven correct. Pancake is one example, a C-like language built for verification from the ground-up. The Lean proofs can talk about the Pancake source, and the verified compiler’s carries them down to the machine code. This allows the TCB to shrink so that the extractor and the C compiler are no longer trusted
In terms of TCB, the deeper the proofs reach, the smaller the TCB, but also the further the departure from today’s software engineering practice.
Hybrid approaches
These options can also be mixed within the same client. A mathy module is particularly well suited to be written and proved in Lean. Whereas a larger module, such as fork choice, or one that uses lots of data strucutres, might benefit from higher-level tools like Aeneas or Pancake.
Discussion: How engineering changes
It’s no news that AI has changed software engineering. But in our case we are dealing with security-critical codebases, and hence the potential shift is even greater.
Interface is still king: All FV approaches require meticulous interface design within clients. Figuring out the simplest interface for separating the pure from the dirty is very important, and it also shapes the formal verification theorems. Fortunately, this has always been the case in software engineering: designing modular systems and clean interfaces has always been what separates a good codebase from a bad one.
Open questions
- Who audits the specs and theorems? Do we prefer spec diversity, or one good spec with lots of eyes on it?
- How is the performance of formally verified components compared to native performance?