An executable formal specification of the EVM · Lean 4
A Yellow Paper you can run.1
The Yellow Paper defined Ethereum in mathematics you could only read. Its living replacement is a program you can only run. Jaune is both at once: twenty-two thousand lines of Lean 4 that state the execution layer precisely enough to prove theorems about — and compile into an interpreter that passes the mainnet fixture corpus, fork by fork, case by case.
Fig. 1 — the current-mainnet gates, verbatim. 5,100 fixture files, 34,005 cases, spanning Prague, Osaka, BPO1, BPO2, and the transitions between them — with zero expected failures on this lane.3
Abstract. Jaune restates the Ethereum execution layer as a single Lean 4 artifact that is simultaneously a specification, an interpreter, and a proof subject. It mirrors execution-specs at a pinned commit and implements Prague, Osaka, BPO1, and BPO2 as first-class rule sets selected from block context, passing 5,100 of 5,100 files (34,005 cases) of the current mainnet corpus. All eighteen precompiles — ecrecover to BLS12-381 to P256VERIFY — are pure Lean, with no FFI and no assumed cryptography. The interpreter is total: the fuel that drives it is proven sufficient from the frame’s own gas, with the tight bound, at the definition site. Its semantic errors are typed rather than stringly, its checked entry points bind an executable snapshot to canonical validated state, and a shrink-only CI budget holds the library at zero panics. The semantics is demonstrated strong enough for real verification — a WETH contract’s solvency is proven to be preserved over every state reachable along a valid configured chain, across scheduled fork activations, through a machine-checked compiler, with an axiom audit in CI. MIT-licensed.
§ 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.
The spec is the executable
The Lean definitions that theorems quantify over — exec, stateTransitionUsing, addBlockToChainUsing — are the definitions Lean compiles into the binary that runs the fixture corpus. There is no reference model to drift out of sync, because each rule of the protocol is written down exactly once.
All the way down to the curves
Every precompile is Lean source: ecrecover, MODEXP, BN254 pairing, the full EIP-2537 BLS12-381 set, KZG point evaluation, and Osaka’s secp256r1 P256VERIFY. There is not one @[extern] in either repository — no linked C, no “assume this crypto is correct” frontier under the theorems.
Trust is checked, not asserted
A no-toolchain CI gate fails the build on any stray sorry. Nothing in either repository uses native_decide, which would move trust out of the kernel and into the compiler. And the flagship theorems have their exact axiom sets printed and checked by CI — propext, Classical.choice, Quot.sound, nothing else.
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
Fig. 2 — sixteen typed error ADTs replaced the strings that used to discriminate semantic outcomes. String survives only at the external parsing, rendering, and fixture-compatibility boundary — 56 allowlisted rows across the whole gate, and the allowlist may only shrink.
scripts/check-integrity.sh inventories every panic, raw bang operation, and stringly-typed semantic carrier in Jaune.lean’s import closure — computed transitively from the module graph, never hardcoded — and demands an exact allowlist row for each. A new occurrence fails the build. Known defects carry an owning step and count against a declared budget that may only decrease, so a step cannot discharge one and quietly introduce another. The library-wide panic count is 0; the pending budget is 0.
CheckedBlockChain binds an executable snapshot to canonical state, hash-linked retained history sufficient for BLOCKHASH, and tip-state-root agreement; ConfiguredChain adds a validated activation schedule and chain-ID agreement, once. Repeated execution reuses those witnesses instead of recomputing a trie root per call — the checked path measured 2.3% faster than the unchecked one it replaced, so the guarantees are not paid for at runtime.
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, and BPO2 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.
inductive Fork : Type | prague | osaka | bpo1 | bpo2 -- BPO1 is Osaka with three numbers changed — 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. -- An unimplemented fork is an error — never a fallback to -- another fork's rules, which would turn a missing -- implementation into a silent consensus fault. def Fork.rules? : Fork → Option ForkRules | .prague => some pragueRules | .osaka => some osakaRules | .bpo1 => some bpo1Rules | .bpo2 => some bpo2Rules
Fig. 3 — forks as data. ForkRules centralises the blob schedule, code and transaction limits, MODEXP pricing, fork-gated opcodes, and the precompile activation set; ChainConfig maps timestamps to forks and rejects ambiguous schedules.
Every executable EIP in the Prague→Osaka delta of execution-specs is implemented and exercised by a strict all-PASS gate — 2,514 of 2,514 files, 17,323 cases:
Fixtures like OsakaToBPO1AtTime15k run through the configured block-import API: each block’s timestamp chooses its rules mid-stream. The transitions suite — Prague→Osaka, Osaka→BPO1, BPO1→BPO2 — is a strict all-PASS gate. Selectors that would match zero fixtures are refused, not reported as vacuously green.
§ 3 Conformance
Tested like a client.
Two fixture lanes. The canonical lane is the execution-specs tests@v20.0.1 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. 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.
| suite | files | cases | result | wall | --jobs auto |
|---|---|---|---|---|---|
| --suite smoke | 16 | 28 | all pass | 0.5 s | 0.5 s |
| --suite prague | 2,573 | 16,573 | all pass | ~12 min | ~3.0 min |
| --suite osaka | 2,514 | 17,323 | all pass | ~8 min | ~2.3 min |
| --suite transitions | 13 | 109 | all pass | 16 s | ~8 s |
| --suite full | 5,100 | 34,005 | all pass | ~19 min | 5.3 min |
Table 1 — the current-mainnet lane (scripts/check-mainnet.sh), blockchain_tests from tests@v20.0.1, verified by SHA-256 at bootstrap. This lane has no expected-failure baseline: every manifested case at a supported fork passes.3 Both harnesses take --jobs auto; the sequential column stays the authoritative one, because a contended run’s per-file timings measure the scheduler rather than the fixture.
| tier | files | committed baseline | what it covers |
|---|---|---|---|
| --depth | 67 | all pass | recursion & call-depth stress |
| --smoke | 174 | 173 pass · 1 expected fail | curated cross-section — the routine gate |
| --bls | 29 | all pass | EIP-2537 BLS12-381 + KZG point evaluation |
| --patch | 10 | all pass | fixed historical failures — un-rebaseable |
| --rlp4 | 4 | all pass | invalid-RLP / header targets — un-rebaseable |
| --full | 2,983 | 2,978 pass · 5 diagnosed non-passes (none a Jaune defect) | the frozen BlockchainTests corpus (8 min at --jobs auto) |
Table 2 — the frozen legacy lane (scripts/check.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, 51 precompile vector files — 1,824 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.
Jaune is not proved equivalent to the Yellow Paper or to execution-specs. That correspondence is established the way every client establishes it — by differential testing against pinned corpora — and published as per-file classifications rather than asserted as a theorem. The formal guarantee is relative to Jaune’s semantics; the empirical guarantee is the corpus. Confusing the two is how verification gets oversold, and this project declines to.
§ 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 remaining gas can never exhaust. theorem execFueled_ne_exhausted (evm : Evm) (fuel : Nat) (h : evm.dyna.gasLeft < 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
Fig. 4 — the sufficiency result, closed 2026-07. A gas-decrease corpus over all 82 instruction constructors feeds a settlement-and-monotonicity argument; exec and the frame-level API (runFrame, executeCode, processMessage) are total, and the "RecursionLimit" observable is deleted from the semantics.
Adequacy between the relational semantics proofs use and the interpreter that runs becomes a clean equivalence — no fuel threshold, no ∃ fuel, ∀ fuel′ > fuel, … plumbing in any statement:
lemma exec_iff_exec_eq : Nonempty (Exec pc sevm devm exn) ↔ exec ⟨pc, sevm, devm⟩ = exn
And the seeding is provably an implementation detail: execFueled_run_mono shows more fuel never changes a reached result, so no semantic choice is hiding in the constant.
Proof-engineering telemetry: the combinator layer discharged 43 of 69 per-instruction obligations in one dispatch; the arc deleted Blanc’s entire fuel-threshold machinery, −113 Fueled mentions across its proof files, with the then-protected four theorem statements byte-identical before and after.
§ 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 instrument, same machine, five-run medians. The 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.
BLAKE2b: 9.72× on the corpus’s worst case
Blake2.g ended in four Array.set! calls. Array α stores boxed elements, so a BLAKE2b round — eight mixes — cost 32 heap allocations and 32 frees, in a loop that does no other memory work. Keccak had solved exactly this one file away, holding its 25 lanes as unboxed scalar fields. Applying it to BLAKE2b took CALLBlake2f_MaxRounds from 753.24 s to 77.45 s — 175.4 to 18.0 ns per round over 4.29 billion rounds — with byte-identical runner output before and after.
The flat round is not trusted, it is proved: two theorems relate it to the retained reference round, with axioms exactly propext and Quot.sound. The old definitions stay in the file — not as dead code, but as the specification the equivalence mentions.
The legacy corpus is latency-bound: its wall time is set by the single longest indivisible fixture, not by the core count. BLAKE2F held that position at 711 s — 41% of the serial total — so no amount of parallelism moved the gate. Unboxing the round handed the bound to loopMul and dropped the whole corpus from ~15 min to 8 min at --jobs auto.
The generalisable part is the diagnostic, not the remedy. The vector suite was latency-bound too, and its dominant file was a batch of 106 independent cases — so it was sharded eight ways, with a checker proving the shards are an exact partition of the source. CALLBlake2f_MaxRounds was one contiguous computation with no independent units inside it. Sharding had nothing to offer it; only making it faster did.
| microbenchmark | before | after | factor |
|---|---|---|---|
| keccak, 64-byte input | 53,721 ns | 1,359 ns | 39.5× |
| secp256k1 signature recovery | 49,188,387 ns | 2,140,882 ns | 22.9× |
| BLS12-381 G2 scalar multiplication | 217,632,365 ns | 13,028,177 ns | 16.7× |
| secp256k1 scalar multiplication | 16,389,080 ns | 1,580,029 ns | 10.4× |
| BLAKE2F, 12 rounds | 5,065 ns | 3,119 ns | 1.62× |
Table 3 — 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 & WETH
What the semantics is sufficient for: WETH solvency across configured forks.
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 — built to carry one real invariant through Jaune’s semantics at every altitude. The contract is WETH, in 329 lines of Blanc. The invariant is solvency: the contract always holds enough ether to honour every balance.
No sequence of valid blocks admitted by a valid configured fork schedule — including histories that cross activations from Prague through BPO2 — can reach a chain state in which WETH is under-collateralised, provided each step satisfies the explicit withdrawal no-overflow bound.
theorem chainUsing_preserves_solvent (wa : Adr) (cfg : ChainConfig) (ch ch' : BlockChain) (h_reach : BlockChain.ReachUsing cfg ch ch') (h_inv : State.Inv wa ch.state) : State.Inv wa ch'.state
Read the quantifiers — ReachUsing is reachability on a valid configured chain: the base carries configuration, context, and chain-ID validity; each step uses whichever fork the schedule activates at that block’s timestamp and carries the withdrawal no-overflow bound. A history crossing Prague, Osaka, BPO1, and BPO2 is one chain of these steps. The invariant survives the hard forks, and that is a theorem, not a changelog promise.
Each layer discharges the assumption the one above it would have to make
Blocks arriving as raw bytes. RLP decoding and the block-hash check live inside the theorem, not in its assumptions — solvency survives from Bytes on the wire to the resulting chain state.
Every reachable state, across activations. Induction over configured reachability — no block sequence of any length under a valid schedule breaks the invariant when each step's explicit withdrawal bound holds.
One whole block, under any scheduled fork’s rules. Every transaction, plus withdrawals, requests, nonce increments, balance transfers, account destruction — with the no-overflow bound carried explicitly.
Any successful execution of the contract. Universally quantified over entry point, calldata, call value, depth, and re-entrant sub-calls — not a case split over the functions someone remembered to audit.
Source to bytecode, backward simulation. Every behaviour of the compiled byte string is a behaviour of the Blanc program — so a property proved about source is a fact about what the EVM executes.
Jaune’s executable semantics. The definitions every rung above is stated over — the same ones compiled into the binary behind the 34,005 passing cases of §3.
def deposit : Func := caller ::: sload ::: -- caller_bal callvalue ::: add ::: -- (call_val + caller_bal) caller ::: -- caller :: (call_val + caller_bal) sstore ::: -- caller balance now up to date logDeposit
-- sum of all WETH balances in storage s def wbsum (s : Stor) : Nat := sum s.rest def Stor.Solvent (s : Stor) (v b : B256) : Prop := wbsum s + v.toNat ≤ b.toNat structure State.Inv (wa : Adr) (w : Jaune.State) : Prop where (code : some (w.getCode wa).toList = Prog.compile weth) (nof : Blanc.SumNof w.bal) (solvent : State.Solvent w wa)
theorem correct (sevm : Sevm) (pre : Devm) (p : Prog) (post : Devm) (exc : Exec 0 sevm pre (.ok post)) (eq : some sevm.code.toList = p.compile) : Prog.Run sevm pre p post
The direction matters: from a real EVM execution of the compiled bytecode, recover a source-level run — so safety proved at the source is a fact about the bytecode the compiler emits, not merely about the source language.
Scope, stated plainly: Blanc’s WETH is a reimplementation, not a model of the deployed WETH9 contract; its observable differences in address decoding, storage, collision handling, and payable entry points are catalogued in the deviation registry. The theorem is about the bytecode this source compiles to. Transferring it to the contract at 0xC02a…6Cc2 would need a separate argument that nobody here has made.
Blanc’s CI prints the exact axiom set of all eight audited theorems — the seven solvency results weth_preserves_solvent, stateTransition_preserves_solvent, chain_preserves_solvent, addBlockToChain_preserves_solvent, stateTransitionUsing_preserves_solvent, chainUsing_preserves_solvent, and addBlockToChainUsing_preserves_solvent — plus the compile witness wethCode_compile, which pins the exact bytecode those theorems are about — and fails on anything beyond propext, Classical.choice, Quot.sound. No sorry, no native_decide, nowhere in the trusted path.
Blanc pins Jaune by immutable commit in its lakefile, so the pair builds reproducibly from two clones — and “which semantics was this proved against” always has a one-line answer.
Blanc is the case study, not the product. It exists to demonstrate — end to end, with no gaps at the seams — that Jaune’s semantics is strong enough to hang a protocol-level economic invariant on. If you want that altitude for a contract of your own, the machinery is MIT-licensed and 6,400 lines of worked example are waiting.
§ 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.
-
Fixed-base precomputation & joint-wNAF for ecrecover gate: ≥15% inclusive in 3 families — measured 8.78–10.42%; deleting recovery entirely capped the win at 1.106×no-go
-
Projective-coordinate Miller loop for BN254 & BLS12-381 pairings gate: ≥20% inclusive in affine double/add — measured 4.14% and 3.42%no-go
-
Byte-layer reroute of the keccak input path gate: ≥15% marshalling residual in ≥2 families — measured 5.1%, 5.5%, 5.5%no-go
-
Flat U256 representation, first attempt archived: word ops measured 0.0–1.1% of the profile at the time; reopens only under a new, separately measured rationalearchived
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.
Regression gates, not green theatre
Committed baselines record the expected PASS/FAIL of every file; a gate passes only on an exact match. Two target tiers are explicitly un-rebaseable, and rebasing any other requires stated scope and justification in the plan — a gate is never weakened to land a change. When an optimization made a baseline’s timings stale, the fix was not to reach for --rebase: that flag was split into two verbs, so “the code got faster” can no longer be spelled the same way as “accept a changed classification.” The safe verb re-derives the classifications from the bytes it is about to write and refuses if any moved.
Every external input is pinned
Fixture corpora never enter the repository: bootstrap scripts provision them against a machine-readable manifest — Git commits for the legacy suites, SHA-256 for release archives, a frozen Python interpreter for the differential oracle — and a read-only environment doctor reports drift without touching anything.
The trusted path is checked mechanically
A no-toolchain CI job fails the build on any sorry or stray dbg_trace outside a justified allowlist; a second job holds panics, raw bang operations, and stringly-typed semantic carriers to a shrink-only budget over the import closure; Blanc’s job prints exact axiom sets for all eight audited theorems. Generated constants and vectors come from named generators, never hand transcription.
§ 8 Trajectory
Recently landed, currently open.
The multi-fork architecture
Fork-parameterised rules, the complete Osaka execution delta, BPO1/BPO2 as schedule data, configured transitions, and the strict-manifest current-mainnet lane — 5,100/5,100 files. The generic transition proof landed in the fork arc; configured reachability and raw-import corollaries are now restored and protected by Blanc’s exact-axiom audit.
Toolchain migration & the totality arc
Lean and mathlib to v4.32.1 with every classification unchanged; then the sufficiency proof — a total interpreter with the tight fuel bound, RecursionLimit deleted, and Blanc’s adequacy bridge restated as an equivalence.2 Then the BLAKE2b unboxing, which moved the corpus’s latency bound off a precompile for the first time.
Semantic-integrity hardening
Seven priority findings from a full internal review, each now a checked invariant rather than a convention — strengthening Jaune specifically as a specification and verification substrate, the role everything else here depends on:
- typed error ADTs throughout the core semantics, with String confined to a shrink-only allowlist at the external boundary;
- checked entry points binding an executable snapshot to canonical validated state, and a wire ingress that a hand-built block cannot reach;
- configured execution that fails closed before a chain’s earliest implemented era, instead of assuming every schedule starts at timestamp zero;
- zero panics and zero partial definitions in the library, mechanically enforced — one of the removals fixed a real bug in twist-coefficient extraction, not merely a totality gap.
A machine interface: t8n
Jaune today is a repository you can inspect and a binary you can hand a fixture. The execution-testing ecosystem already has a standard way to invoke an EVM — the transition-tool interface — and Jaune is absent from that list because it consumes filled fixtures rather than exposing the protocol. A read-only spike found the seam already exists: the body executor never sees a header, so t8n is “build the environment, run the body, emit the roots instead of comparing them,” with no new semantics. The frontend lives outside the proof-facing import closure, so no proof client can come to depend on it. Planned, not built.
The allocation economy
Roughly 40% of interpreter loop time is memory management — 47–57% of busy samples are allocation and reference counting on the current runtime. Ownership and in-place-update discipline comes first (zero proof exposure); representation changes to B256 and the stack sit behind their own measured decision gates, because they touch types Blanc proves over directly. Jumpdest validity — a static property currently re-derived at every jump — rides along with whichever session next opens the interpreter.
More of the protocol under proof, more contracts over it
WETH is the existence proof, not the destination. The open questions are which contract-level invariants justify their proof effort, how much block-level reasoning is reusable across contracts, and where a proof-first language stops being expressive enough. Collaborators with a target property in mind are exactly who this page is for.
§ 9 Who this is for
Three ways in.
Proof engineers & PL researchers
A live, non-toy verification target: ~39,000 lines of Lean 4 spanning an executable semantics, a verified compiler, and a chain-level invariant — with well-posed open problems in representation choice, proof-exposure budgeting, and fork-parameterised reasoning. The sufficiency arc alone is a worked case study in retrofitting totality onto a large fueled interpreter.
then: Blanc/Solvent.lean → the theorems of §6
Protocol & client engineers
An independent implementation of the Prague-through-BPO2 rules that reads as a specification and runs the real corpus — a differential oracle, a precise reference for when a fixture disagrees with your client, and a place where each rule is stated once, without the surrounding engineering.
scripts/check-mainnet.sh --suite smoke in 0.5 s
Security researchers & DeFi builders
Invariants that hold at chain level, not per function. A fuzzer searches for the counterexample; this is the other half — a machine-checked proof that, for a stated invariant and contract, no counterexample exists in any reachable state, under any fork schedule.
Blanc/Solvent.lean — 6,400 lines of why it holds
§ 10 Reproduce it
Two clones and a build.
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.
Jaune
run the spec against real fixturesFixture corpora are provisioned separately by checksum-verified bootstrap scripts — see scripts/vectors/SOURCES.md for pinned provenance, disk requirements, and the read-only environment doctor. Every gate’s exact command, scale, runtime, and pass criterion is catalogued in scripts/GATES.md; the fixture harnesses take --jobs auto, which puts the whole current-mainnet corpus inside a coffee break.
Blanc
check the proofs yourselfcheck.sh builds the library and runs the axiom audit over all eight audited theorems — the seven solvency results plus the WETH compile witness; it exits non-zero if any of them acquires sorryAx, ofReduceBool, or ofReduceNat.
- Successor in spirit, not in office. Jaune is an independent project with no affiliation to the Ethereum Foundation. Ethereum’s canonical specification is execution-specs, which Jaune mirrors at pinned commit 4198b9c5 (mainnet branch, 2025-09-19) and tests against. ↩
- Jaune was previously published under the name ELeVM; the repository was renamed in July 2026 and old links redirect.
- Figures on this page are drawn from committed reports, baselines, and benchmark instruments in the repositories, current as of the 2026-08-01 semantic-integrity closure. Wall-clock numbers are same-machine, same-instrument measurements on a 10-core Apple M5; fixture counts are exact. The current-mainnet lane covers every blockchain_tests fixture of tests@v20.0.1 whose fork Jaune supports; exclusions for unsupported historical forks are machine-generated with per-fork reasons, and unknown labels fail the manifest check.