A Yellow Paper you can run.¹

§ 1 The gap this closes

One artifact instead of two.

Formal models of the EVM are usually written for the prover — small, idealised, and quietly different from anything that runs. The distance between the model and the implementation is where the bugs live, and nothing in the proofs covers it. Jaune removes the distance by refusing to have two artifacts.

A specification substrate has to be sound before it is fast

An internal review found seven ways this artifact could still have been a good interpreter and a bad specification: a chain that paired a tip with an unrelated state, a hand-built transaction indistinguishable from a wire-decoded one, an unimplemented era silently answered with another fork’s rules, error strings doing the work of a datatype. All seven are closed, and the gate that keeps them closed is the interesting part.

-- The VM's whole error carrier. An internal defect cannot be
-- mistaken for an expected halt, because it is a different
-- constructor rather than a different string.
inductive EvmError : Type
  | halt (reason : ExceptionalHalt)
  | revert
  | crypto (reason : CryptoError)
  | internal (reason : InternalError)

-- What a settled frame may store. `crypto` and `internal`
-- are unrepresentable here by construction.
inductive SettledHalt : Type
  | halt (reason : ExceptionalHalt)
  | revert

-- Checked wire ingress: a private constructor reachable only
-- through the strict decoder, carrying its own round-trip
-- evidence, so a hand-built Block cannot be certified.
def CanonicalBlock.ofRlp? (raw : Bytes) : Option CanonicalBlock

Lineage, stated plainly: the Yellow Paper has not kept pace with the protocol, and Ethereum’s canonical specification today is execution-specs — executable Python, current, but not a thing you can state a theorem in. Jaune mirrors it at a pinned commit, tests against its fixtures, and adds the property neither ancestor has: the text of the specification is itself a mathematical object inside a proof assistant.

§ 2 Coverage

The protocol, present tense.

A specification earns the name only while it describes the protocol that actually exists. Jaune is fork-parameterised: Prague, Osaka, BPO1, BPO2, and Amsterdam are values of one ForkRules record, and a single interpreter reads the record and nothing else. A chain’s configuration schedules activations; each block’s timestamp selects its rules. Every machine carries its fork, so rule validity is proved once, for all five, rather than assumed at each use.

inductive Fork : Type
  | prague
  | osaka
  | bpo1
  | bpo2
  | amsterdam

-- BPO1 is Osaka with its blob schedule replaced — enforced by
-- construction, so no BPO fork can silently acquire an
-- execution rule of its own.
def bpo1Rules : ForkRules :=
  { osakaRules with fork := .bpo1, blob := bpo1BlobSchedule }

-- The single place a fork identity becomes rule data. Total:
-- a Fork is the selection of one of five rule records, never
-- an identity that may fail to resolve or fall back to
-- another fork's rules.
def Fork.ruleSet : Fork → ForkRules
  | .prague => pragueRules
  | .osaka => osakaRules
  | .bpo1 => bpo1Rules
  | .bpo2 => bpo2Rules
  | .amsterdam => amsterdamRules

theorem Fork.ruleSet_valid (f : Fork) : f.ruleSet.Valid
theorem Fork.supported_eq_all : Fork.supported = Fork.all

§ 3 Conformance

Tested like a client.

Three fixture lanes. The canonical lane is the execution-specs tests@v20.0.2 release under strict generated manifests: activating a fork means its whole suite, exclusions are machine-generated with per-fork reasons, and unknown labels fail loudly. A separate devnet lane runs Amsterdam against its pinned prerelease corpus under the same rules, sharing nothing with the mainnet lane’s pin, manifest, or install. The frozen ethereum/tests lane is retained as an independently-filled regression instrument with committed per-file baselines. Its five non-passing files are diagnosed, and none is a defect in Jaune.

Table 1 — the current-mainnet lane (scripts/check-mainnet.sh), blockchain_tests from tests@v20.0.2, verified by SHA-256 at bootstrap. This lane has no expected-failure baseline: every manifested case at a supported fork passed in the full-lane run of 2026-09-21.³ The timing columns were measured on the tests@v20.0.1 corpus, not the updated one: the --jobs auto column on 2026-09-21, after the Lean 4.34 migration; the sequential column earlier. Both harnesses take --jobs auto. Uncontended per-file timings require sequential runs.

Table 2 — the Glamsterdam devnet lane (scripts/check-mainnet.sh --lane amsterdam), over tests-glamsterdam-devnet@v8.1.4, with zero exclusions inside the Amsterdam trees. The four findings are the invalid pre- and post-fork blocks of the SLOTNUM and block-level-access-list transition modules: their headers carry 22 RLP fields, which Jaune rejects as a structural encoding error where the fixtures name a block-format, access-list-hash, or block-hash exception — same verdict, a different name for it. The union ran in 463.6 s at --jobs auto on 2026-09-21, red on exactly those four files.

Table 3 — the frozen legacy lane (scripts/check-legacy.sh). Each gate passes iff every file’s PASS/FAIL matches its committed baseline — a regression gate, not an all-green banner. None of the five baselined FAILs is a defect in Jaune: two fixtures carry no case in the supported fork range, and the other three are multiply-invalid cases whose expected-exception alternatives reflect another client’s check ordering and omit the identity Jaune reports — the same one the frozen oracle reports. Within this corpus the GeneralStateTests/ subtree passes 2,633 of 2,634.

Beneath the fixture lanes sit three oracles. Two are differential against a frozen execution-specs Python interpreter — 21,593 word-arithmetic and hash cases, and 240 blob-fee taylor_exponential cases. The third checks the elliptic-curve layer on 573 pinned, differential, and algebraic-identity cases, with no skip and no unknown outcome. Alongside them, 53 precompile vector files — 1,990 cases, including 782 for P256VERIFY — run under a strict manifest that fails on a missing or unexpected file, and on a file that runs fewer cases than it declares. A vector file that quietly lost half its cases would otherwise pass while testing half as much. And since 2026-08 the interpreter also answers as a standard t8n transition tool: scripts/check-t8n.sh compares its complete output on 39 cases — 30 of them Amsterdam’s, block-level access list included — against goldens from the pinned execution-specs, with every normalization and deviation explicit and each case run twice for determinism. A three-way acceptance run against go-ethereum in 2026-08 found that in every registered divergence, Jaune matches its pinned conformance target. Read the case study: what a full-output reader sees in t8n.

§ 4 Totality

A total interpreter, proven so.

Executable semantics in a proof assistant usually carry a fuel parameter, and “out of fuel” leaks into every downstream statement as a side condition. Jaune closed that door: the EVM’s own gas bounds its recursion, and the bound is a theorem, not a convention.

-- Fuel strictly above the gas measure can never exhaust.
-- The measure is gasLeft plus any spilled Amsterdam state
-- gas; on every earlier fork it is exactly gasLeft.
theorem execFueled_ne_exhausted (evm : Evm) (fuel : Nat)
    (h : evm.dyna.gasMeasure < fuel) :
    execFueled evm fuel ≠ Fueled.exhausted

-- The additive constant is 1 — the tight bound.
def sufficientFuel (gas : Nat) : Nat := gas + 1

-- The total interpreter. Fuel is an implementation detail,
-- discharged by proof at the definition site.
def exec (evm : Evm) : Except (EvmError × Devm) Devm

lemma exec_iff_exec_eq (pc : Nat) (sevm : Sevm) (devm : Devm) (exn : Execution) :
    Nonempty (Exec pc sevm devm exn) ↔ exec ⟨pc, sevm, devm⟩ = exn

§ 5 Performance

Fast enough to check.

A specification nobody can afford to run is a specification nobody checks. Two measured optimization arcs — elliptic curves, then keccak — took the four-family benchmark aggregate from 105.81 s to 11.5 s on identical instruments and hardware, a 9.2× speedup, without changing a single baseline classification, gas rule, or public signature. A third then took the single slowest fixture in the entire corpus from 12½ minutes to 77 seconds.

Fig. 5 — same four fixture families, same machine, summed per-file seconds, each bar from its arc’s committed report; the last is the best of three runs. The v4.32.1 toolchain migration, the totality arc, and the semantic-integrity arc each re-measured and landed at parity or better — the BLS tier 20.6% faster after migration, the checked-entry-point path 2.3% faster than the code it replaced. The last bar is the most recent committed run of this instrument; it predates the Lean 4.34 migration and Amsterdam’s metering.

Table 4 — committed benchmark instruments, five-run medians. All of it pure Lean before and after: the speedups came from representation and algorithm, never from calling out to C. The last row is reported at its honest magnitude: twelve rounds behind a fixed per-call cost is setup-dominated, so it dilutes a ~10× round loop to 1.62× and is a corroborating signal rather than the headline. The fixture-level measurement is.

§ 6 Case study — Blanc & the Lido CircuitBreaker

What the semantics is sufficient for: a deployed guardian’s registry, coherent at every reachable future.

The claim that a semantics “supports verification” is cheap until someone pays it. Blanc (fr. “white”, as in whitepaper) is the payment: a deliberately minimal contract language — four constructors, a compiler into EVM bytecode, a machine-checked compiler-correctness theorem — that carries real invariants through Jaune’s semantics at every altitude. Its deepest single exercise of the semantics is a port of the CircuitBreaker that Lido deployed in 2026: an emergency brake whose admin grants pauser addresses time-limited authority over registered protocol contracts. The invariant is Registry integrity: the guardian’s book of authorizations stays coherent, whatever any contract it talks to does.

theorem chainUsing_preserves_registryStable (dp : DeployParams) (ca : Adr)
    (cfg : ChainConfig) (checkpoint future : BlockChain)
    (reach : BlockChain.ReachUsing cfg checkpoint future)
    (stable : RegistryStable dp ca checkpoint.state)
    (hcov : ∀ t f, cfg.forkAt t = .ok f → CoveredFork f) :
    RegistryStable dp ca future.state

Read the quantifiers — ReachUsing is the same configured-chain reachability the WETH solvency family climbed first: whole valid blocks, every transaction anyone sent, arbitrary contracts doing arbitrary things, under the model’s explicit per-step bound on total ether plus withdrawals. RegistryStable packages exactly two facts — the exact compiled runtime is installed, and the contract’s actual storage admits a coherent Registry witness. CoveredFork is exactly Prague, Osaka, BPO1, and BPO2: Blanc now builds on a Jaune that implements Amsterdam, and states its results for the four forks its proofs cover rather than for Amsterdam blocks it has not yet reasoned about. What the theorem does not ask for is the point: a pause hands control to an arbitrary callee mid-transaction, and no hypothesis constrains it. The checkpoint is not assumed either: a deployment theorem walks the official constructor input through Jaune’s real creation-message, transaction, and Prague-block pipeline to establish it.

Each layer discharges the assumption the one above it would have to make

§ 7 Method

Pre-registered gates, and the discipline to lose.

Every number on this page comes from a committed report, baseline, or benchmark instrument. Optimization arcs declare their measurement method and GO/NO-GO threshold before the experiment, and a failed gate cancels the work no matter how much was already invested. Below is the part most projects never publish: the ledger of ideas that lost.

The gates cut the other way too, and the same rule applies: the BLAKE2b arc predeclared GO at ≥2.0×, HALT below — with the recorded response to a low number being “report and stop,” not “reach for a faster form until the number looks better.” It measured 9.72× and shipped. Both halves of that arc were checked with deliberately broken negative controls, run and reverted without ever entering a commit: one wrong word index in the flat round, to confirm the equivalence proof actually fails; one flipped PASS in a baseline, to confirm the timing-refresh mode writes nothing and exits non-zero. A gate nobody has watched fail is not yet evidence.

§ 8 Trajectory

Recently landed, currently open.

§ 9 Who this is for

Three ways in.

§ 10 Reproduce it

Two clones, a build, and a corpus.

The only prerequisite is elan, the Lean toolchain manager — exact Lean and mathlib versions are pinned in the repositories, and Blanc pins Jaune by immutable commit.