Lean mirrors of the Ethereum execution specifications
Everything we state about a contract rests on a precise meaning for the machine it runs on. Ours is a set of Lean 4 mirrors of Ethereum's Python execution specifications, written function for function from a pinned commit. Each mirror records the hash of every Python file it follows, and a mechanical check lists every place the Lean departs from the Python.
A mirror is validated by that correspondence check and by the official tests. The mirrors themselves contain no theorems and no axioms.
Status by fork(as of 15 November 2026)
| Fork | Tests | State tests | Blockchain tests | Last run |
|---|---|---|---|---|
| Amsterdam | official release tests@v21.0.2 | 16,908 pass, 0 fail | 26,349 pass, 0 fail | 2–6 Nov 2026 |
| Osaka | official release tests@v21.0.2 | 14,665 pass, 0 fail | 17,441 pass, 0 fail | 6 Nov 2026 |
| Prague | official release tests@v21.0.2 | 13,919 pass, 0 fail | 16,538 pass, 0 fail | 6 Nov 2026 |
| Cancun | legacy state tests | 3,764 pass, 0 fail, 24 not run for named reasons, of 3,788 | not in the gate | 4 Nov 2026 |
Across Prague, Osaka and Amsterdam: 45,492 state entries and 60,328 blockchain tests, with no failures.
Read these numbers with care
- An invalid block counts as passing when it is refused, as in the Python test runner. It does not show the block was refused for the reason the test names.
- Amsterdam is still changing upstream. Our pin is from early November.
- Cancun has not been run against the newer test release.
- Hash functions (Keccak and SHA-256) are calls into C code, not Lean.
- The mirrors are not yet public. We give read access on request.
The specification language itself
The execution specifications are written in a subset of Python. We also have a Lean semantics of that subset. With it we execute all 148 Cancun opcode handlers from the specification's own source and prove what each one computes. The call and create family still rests on named hypotheses.
Why a second implementation is useful
An independently written implementation cannot decide what is correct. It can find disagreements. If you maintain a specification, a client or a prover and would find disagreement reports useful, write to us.