EVM Sail¶
An executable, machine-checked specification of the Ethereum execution layer, written in Sail — and a workbench for asking hard questions about the guests that prove it.
One source defines the state transition function. From it we extract a reference implementation in C, proof objects for Lean and Rocq, an executable Python rendering, and a research-centric optimised zkEVM guest — through a custom Sail compiler that lowers the specification's semantic types to machine representations.
What this is for¶
Precision. Protocol quantities carry their real limits in their types: a stack height is not an integer that happens to stay under 1024, it is a value whose type says so. Every operation must show its result still lies within those bounds, and the compiler proves it — each type and range obligation is discharged by an SMT solver at compile time.
Verification. The impure boundary is small and enumerable — hashing, input, output, the state stores — and proof targets receive exactly those as axioms, with everything else as ordinary definitions.
Verifying the binary. Extraction still leaves a compiler between the specification and the machine code. Closing that gap is the end goal, and two routes are being explored: binary analysis against authoritative ISA semantics in the style of Islaris, and verified construction as in evm-asm.
Measurement. A zkEVM guest is priced in retired instructions, which inverts much of the usual performance intuition. We instrument this guest and its peers with the same semantic phases on identical inputs, so "where does the cost live?" has an answer with numbers attached.
Optimisation. The fast guest is compiled from the same text as the proofs, not written beside it. A refinement replaces a body with a faster one, never with an assumption — so no optimisation ever becomes an axiom.
Generality. Nothing about verifying a stateless validator is specific to our guest, so the tooling is built to extend to others.
Where to start¶
- Spec — the state transition, the EVM, gas, the tries, and stateless validation.
- Spec extractions — how one source becomes C backends, Lean and Rocq developments, and a Python rendering.
- Research — the compiler, the extraction toolchain, the cost model, and what the experiments showed.
- zkEVM benchmarks — this guest against reth and ethrex, broken down by execution phase.
Status¶
Experimental. A research vehicle, not production consensus software; interfaces and internals change frequently.
Built with AI. Substantial parts of the specification, compiler, and tooling were written with AI assistance under human direction — so treat what you read here as something to check against the corpus gates and the published measurements.