To quickly chime in:
(i) Do we have authoritative formal specifications against which we could verify entire clients?
(ii) What amount of trusted code and assumptions would be required to do so?
(iii) How practical would it be to do so relative to the cadence of changes in client code? This is hard to answer relative both a lack of representative examples of this specific work and assumptions about the progress AI will make, so I’ll ignore it for now but it’s worth keeping in mind.
The answer to (i) is negative. The best set of specifications we have are the Python specifications, which are informal. We have a number of formal specifications in various languages, including, but not limited to, Lean, HOL4 (see Ramana’s post above), and Sail, but these do not cover the whole client specification, typically only the core EVM component – many of the formal specifications originate from the desire to verify smart contracts – or what is needed to specify the zkVM guest program (i.e. the Ethereum state transition function). This does not include other critical components of the clients, such as state for example, which are extremely optimised and in which bugs have previously happened.
On the consensus side, the Nyx Foundation has been working on Lean specifications for a leanEthereum consensus client but I’m not sure what the status is there.
The answer to (ii) depends heavily on the source language in which the clients are written or the possibility to verify compiled binaries for all relevant architectures (at the very least x86, aarch64, rv64im for zkVM guest programs). Let’s split this up a bit more.
First, one has to think about which representation of the code is going to be verified, anything from the high level source code, which is in principle easier to reason about but will require language specific tooling, to a compiled binary, which will be harder to reason about (also depending on the source language and associated compiler) but where the tooling would not be required to be specific to the high level language.
If we consider the languages in which clients are written, we have to look at the following languages: Go (Geth, Erigon), C# (Nethermind), Java (Besu), Rust (Reth, ethrex) on the execution, and Rust (Lighthouse, Grandine), Typescript (Lodestar), Nim (Nimbus), Go (Prysm), Java (Teku) on the consensus side. (Apologies if I’ve forgotten any relevant client.)
Rust is a highlight of this list because it both provides higher assurances out of the box as far as safe Rust is concerned and because it also has an active set of verification tools built for it (see for example hax, Aeneas, Verus, and others which are used for production code deployed at scale). These are not silver bullets: you still need specifications and, as Rust lacks any authoritative formal semantics, extracting (subsets of) Rust to a formal proof friendly representation is trusted and bugs in these extractions happen. The fact that these tools only handle a subset of Rust code also has important limitations: there is no guarantee your Rust codebase, even if it is in pure safe Rust, will extract without requiring modifications to the code. Indeed, on the cryptography side, extracting code from libraries like plonky3 and zkVM codebases has been a struggle (although it has improved recently). Whilst the Rust compiler provides memory safety assurances (which mean memory safety is typically not verified, a huge reduction in workload), it is not itself verified and compilation could change the semantics of the high level code that is verified.
The situation is worse for the other languages in that there is simply less tooling available as far as I know, the compilers offer fewer assurances, and the issue of lack of formal semantics is consistent across the board. Nethermind have proposed that there be C# semantics formalised in Lean, which would greatly help develop tooling to verify C# code in Lean, although the other issues would remain; in particular, since compiling C# down to RISC-V zkVM targets requires working around limitations of the standard .NET compiler, there is another reminder to consider the assurances we can provide about such general purpose compilers which are hard to verify. Mike Dodds has some ongoing work targetting Go but I don’t know how validated it is.
If instead we consider looking directly at binaries, which as the benefit of being a more uniform task across the range of languages used to develop clients and the possibility of providing higher assurance by removing the compiler from the trusted code base, we still find the issue of lacking specifications, including in this case with respect to the additional need for specifications of the corresponding ISA. Sail has specifications for RISC-V and x86 as well as Lean, HOL4, Rocq, and Isabelle backends (among other great tooling) but not aarch64 (Arm uses its own ASL language). ACL2 has a fantastic x86 specification (which can boot linux!), which is also the source for Sail’s x86 specification. Proofs at this level are also much harder because the representation being analysed has much less helpful structure. Brute-forcing this with AI is one option, but some first look at this (e.g. by Cody on the EF Research Engineering team) points towards limitations and token inefficiency issues; we must remember that ideally we’d want to verify several clients which all continue to evolve. Approaches based on decompilation may be helpful, and we are aware of some work towards a decompiler in Lean but have not yet evaluated it.
Another approach is to consider implementing a client in low level code, using a proof assistant like Lean as the macro assembler. This is what we’re pursuing with evm-asm which aims to implement a zkVM guest program directly in RISC-V assembly with proofs against a Lean specification and verified code generation. AI makes this possible, but development is still not free (it takes time, tokens, and consistent steering of the agents) and, as always, the issue of spec validation remains present.
One could also aim to produce a client by directly compiling from a specification (or an optimised refinement of one) via a verified compilation pipeline (see for example CertiCoq and more recently the work on Peregrine that extends this approach to other proof assistants), but we would need to assess any performance losses that happen as a result. There was some work towards this in Rocq, but I would need to get an update on it to see whether we have anything to benchmark at this point.
, to keep the formal spec in sync automatically as forks change. Your point (iii) about client cadence makes a strong case to build this.