Blanc/How it works
From bytes to theorems.
Blanc’s results are built in layers: Jaune’s semantics of the whole machine; a reading of the bytes that the kernel checks; generic tools for proving things about that reading; a model, an invariant and a deployment for each contract; and theorems at four levels of execution, from one call frame to an arbitrary history of blocks. This page walks the layers, then says exactly what the kernel checks and what it cannot.
Layer one
The semantics: Jaune.
Jaune is an executable formal specification of the EVM and of Ethereum block processing in Lean 4, first written from the Yellow Paper and then rebuilt on a pinned 2025 revision of Ethereum’s executable specification, execution-specs, with Osaka and the two blob-parameter forks implemented from their EIPs. Its library of about 45,500 lines defines the machine, all transaction types, block validation, the processing of system calls, withdrawals and requests, every precompile from ecrecover to the BLS12-381 operations and P256VERIFY, and the selection of fork rules by a chain’s activation schedule. The same definitions run against test fixtures and appear in proofs.
tests@v20.0.2 passsorry or foreign functionConformance. Jaune’s current-mainnet lane runs the blockchain tests of the fixture release tests@v20.0.2 and requires every one whose forks lie among Prague, Osaka, BPO1 and BPO2, transitions included, to pass; the selection comes from the fixtures’ own network labels, and the run fails if anything selected fails or if nothing is selected. At the revision Blanc pins, all 5,006 selected files pass, holding 34,205 cases: 16,673 for Prague, 17,423 for Osaka and 109 across transitions, 47 of them crossing into BPO1 or BPO2. On the legacy ethereum/tests corpus, Jaune’s documentation records 2,978 passing files of 2,983 and diagnoses each exception.
One function for tests and theorems. Blanc’s history theorems quantify over runs of stateTransitionUsing, Jaune’s configured block transition, and the fixture runner imports each block through a function whose core, stateTransitionE, stateTransitionUsing also reaches. The fixtures therefore test, as compiled code, the per-block transition the theorems describe. What the configured transition adds, a check of the chain’s identity and the choice of fork by the block’s timestamp, the runner performs with the same functions only in the 109 transition cases; a single-fork fixture takes its fork from its label.
Forks. Prague, active on mainnet since 7 May 2025, and Osaka, BPO1 and BPO2, which followed it, are the four forks that have governed mainnet since. Jaune implements each as a complete record of rule data, selected per block by the chain’s schedule. It also implements Amsterdam, the next upgrade; no theorem here is stated for it.
Trust surface. Jaune’s library contains no axiom, sorry, native_decide, @[extern], opaque, partial or implemented_by, as a check in Jaune’s repository enforces, with one allowlisted @[csimp] substitution proved equal to the definition it replaces. Its optimized SHA-256 is proved equal on every input to a transcription of NIST FIPS 180-4, in a module outside Blanc’s import closure, so Blanc’s axiom walk does not cover that theorem. For Keccak-256, only the optimized permutation is proved equal to a reference transcription; the transcription’s conformance to the standard rests on test vectors and the fixtures — one reason no theorem here relies on Keccak’s quality as a hash function.
Layer two
Reading bytes as a program.
EVM bytecode has no structured control flow: a JUMP takes its destination from the stack, and compilers implement internal functions by jumping through pushed return addresses. Recovering the structure is a heuristic task, long studied by decompilers, and Blanc does not trust whatever performs it.
A certificate is a list of entries. Each gives a program counter, an abstract stack of the operand words above the current function’s base — each a known constant, the function’s own return address, or unknown — and a tree over a small instruction language whose nodes correspond one to one with instructions of the bytes: straight-line instructions, branches, gotos, calls of internal functions with their continuations, returns and halts. A 2,836-line Python program proposes certificates from the raw bytes, and nothing it does can make an unsound certificate pass. The eight artifacts’ runtime certificates range from 7 entries, for the EIP-7002 contract, to 211, for the vulnerable Vyper pool.
The trust boundary is a Lean function, Cert.check, which walks every tree against the literal bytes. It checks that each node’s instruction is the one encoded at that position, tracks the abstract stack with a transfer function proved sound against Jaune’s semantics, and requires every jump to land on the constant destination its tree names and every call and return to pair up through a constant return address. A companion, Cert.jumpsOk, confirms every jump target is a valid jump destination, which liveness needs. The checks are closed by evaluation in Lean’s kernel, split into parts that each fit in memory, and a gate regenerates every registered certificate from its committed input and compares it byte for byte.
New producers of bytecode have needed small, general extensions rather than new trust, each proved sound once for all certificates: a conditional jump whose taken side is a back edge, for WETH9’s loops; constant folding, nodes that push their own program counter, decided conditional jumps and a variant that tracks a constant memory map, for the vulnerable Vyper pool; and folding of the AND with which solc 0.5.16 masks internal function addresses, for the Uniswap pair. The hand-written EIP-7002 contract needed none. The design is translation validation run backwards: it validates a decompilation instead of a compilation, so the producer is free to be clever, and to change, without entering the trusted base.
Layer three
Proving things about the reading.
Three generic theorems, proved once for all certificates, turn a passing check into reasoning power.
- Safety. Every successful execution of the bytes from program counter 0, on a covered fork, is a run of the certificate’s program, so safety properties of the program hold of the bytes.Blanc.Lift.lift_sound
- Liveness. The converse: every gas-exact run of the program is a successful execution of the bytes.Blanc.Lift.lift_exact
- Every outcome. The certificate cursor places every node of a frame’s execution at a checked point of the certificate, whatever the frame eventually does; no statement about it has a success premise.Blanc.Lift.cursor_of_parentPrefix
Per-contract proofs then use three kinds of walk. Inversion walks establish safety: from a successful run of a tree node, a lemma for each kind of instruction recovers the successor state, and chaining these along a function’s tree replays every path the bytes can take; loops — the EIP-7002 fee series, the Uniswap pair’s Babylonian square root — are walked by induction. Exact walks establish liveness and its cost, building a gas-exact run forward one node at a time. Each step lemma is stated backwards, with its charge written as a numeral wherever the charge is fixed, so that applied to a goal whose gas is g + N, Lean’s unification of natural-number offsets solves the continuation’s gas, and the gas obligations of a walk disappear into unification. The cursor serves statements about executions of any outcome: a lock must stop reentry even into a frame that later reverts.
A fourth tool serves locks. For the fixed Vyper pool, a second Boolean pass over the certificate, with the lock’s state at join points supplied by a 444-line untrusted annotator, decides that every guarded body is reached only after the lock was found free, that every mutating body starts with the lock held, and that inside it only release points write the lock’s slot; a soundness theorem along the cursor connects the pass to every frame that runs the code from its first instruction on a covered fork, provided the hashes the frame computes avoid the lock’s slot.
Layer four
Four levels, and the configured history.
Blanc states results at four levels. A frame theorem concerns one execution of the contract’s code from program counter 0. A message theorem concerns Jaune’s message processing, including child frames, reverts and settlement. A transaction theorem concerns processTransaction, with validation, intrinsic gas, refunds and fees. A history theorem concerns a chain.
A ConfiguredHistoryTrace cfg checkpoint future is a sequence of block transitions under the chain configuration cfg, from checkpoint to future, each retaining the evidence of its own execution: the fork the block’s timestamp selected, a proof that this fork is covered, the successful run of stateTransitionUsing, and the retained trace of the block body, with its system calls, transactions, withdrawals and requests, down to every interpreter frame — including frames whose effects were later rolled back. Quantifying over traces loses nothing, since every reachability derivation of the configured chain under covered forks has one, and everything on such a chain is in scope: other contracts, reentrant and reverted calls, system calls and withdrawals.
Extracting a history, not abstracting it
Exactly what was committed.
A history contains calls whose effects did not survive: a frame that reverted, or one that succeeded under an ancestor that reverted. Jaune records settlement, and Blanc extracts from a configured history the list of settlement-committed calls to a contract, in execution order. This is what makes the history theorems exact. For WETH9, the ledger read from storage after any history equals the model’s ledger run over exactly the committed non-static writer calls: rolled-back frames are absent, view calls contribute nothing, and a call re-entered from inside a withdrawal’s ether transfer is placed after the withdrawal that made it. The Uniswap pair needs a nested form, because it calls tokens and a callback that may call it back: its replay consists of steps, one for each outermost committed call, each consuming the committed calls to the pair made during it, and an equation places every committed call in exactly one step.
The opposite choice is right for locks. The reentrancy theorems quantify over Jaune’s raw execution tree, every frame whatever its outcome: a callee that later reverts has still executed. And where a contract depends on other contracts’ answers, those answers become inputs of the statements rather than assumptions about every possible callee — the approach the Uniswap page describes.
No axiom about Keccak
Hashes without added axioms.
Solidity and Vyper keep mappings at hashed storage slots, such as keccak256(a ‖ 3) for balanceOf[a], and a proof about such storage must know that the slots it reasons about are distinct, from each other and from the fixed slots. One shortcut is to assume Keccak-256 injective, which is false: the hash maps an unbounded domain into 2256 values. Blanc adds no axiom about Keccak: each theorem states as a premise exactly the separation facts its proof uses, over finitely many slots wherever it can.
| Kind of premise | What it says | Where |
|---|---|---|
| None | The layout is fixed, and nothing is stored at hashed slots. | Deposit contract, EIP-7002 contract |
| Trace-local | Each key the history may touch is tracked already or lands on a slot in no use, and distinct keys land on distinct slots: a fact about finitely many concrete hash values, which anyone holding the history can compute. | WETH9, 3Crv, Uniswap pair; the fixed Vyper pool, per execution: no digest it computes equals 0, the lock’s slot |
| Decided | With concrete keys, separation becomes computation: a decidable check with an exact soundness theorem, closed by the kernel evaluating Keccak. | CircuitBreaker finite tier; the 3Crv deployment theorem, which computes the hashed slot its constructor writes |
| Universal | Separation quantified over all 2160 addresses. Under a random-function model the failure chance is about q·2−94 per frame — a heuristic, with no reduction or bound proved. | CircuitBreaker history tier; one WETH9 solvency statement, kept beside its trace-local results |
A trace-local premise is not implied by computational collision resistance, and no reduction is proved. It is also necessary: for WETH9, a written allowance slot coinciding with a tracked balance slot breaks backing, and Blanc proves it.
Safety’s dual
Exact gas, and the liveness ladder.
Safety is proved by induction over executions that exist; liveness requires exhibiting one, and on the EVM whether one exists depends on gas. Jaune meters gas exactly — memory expansion, warm and cold access, refunds and the 63/64 rule included — and Blanc’s liveness theorems state costs exactly: for WETH9 a closed formula; for the deposit contract an explicit sum whose terms depend on the deposit’s position in the tree; for the Uniswap pair a closed expression in the access charges of the actual slots and the gas forwarded to each callee; for the EIP-7002 contract a fixed charge plus 87 gas per iteration of the fee loop plus the actual storage accesses; for 3Crv an exact cost the proofs construct but the exported theorem leaves existential.
| Rung | What it says | Reached by |
|---|---|---|
| Frame | A fresh frame with enough gas succeeds and costs exactly the stated amount. | WETH9, deposit contract, 3Crv, Uniswap pair, EIP-7002 contract |
| Model | A call the model accepts is realized by an execution ending in the model’s next state. | the same five |
| Reachable state | The same at the final state of any configured history. | the same five |
| Transaction | A signed transaction is admitted by processTransaction and succeeds, with gasUsed in closed form. | WETH9 |
A function whose success depends on an external call can be live only conditionally, since the callee can revert or consume everything forwarded to it. Blanc states those premises explicitly and nowhere else: WETH9’s withdrawal to a contract assumes the call succeeds, leaves at least 1,489 gas and changes none of WETH9’s storage; 3Crv’s set_name assumes the minter’s owner() answers; six of the Uniswap pair’s functions take the replies and returned gas of their calls. Withdrawal to an account without code needs no such premise. The theorems prove admission and execution, not inclusion: whether any block will include a transaction is outside them.
Where histories start
Deployment.
An invariant stated at a checkpoint is useful only if some real state satisfies it. For WETH9, the deposit contract, 3Crv and the EIP-7002 contract, Blanc executes the recorded creation input of the actual deployment transaction as a CREATE message, under every covered fork, and proves that it succeeds, installs exactly the certified runtime, and leaves storage satisfying the history theorems’ checkpoint invariant, with no hash premise. These deployment theorems, and the CircuitBreaker’s, also prove in the kernel — by evaluating the RLP encoding and Keccak-256 — that the recorded deployer and nonce yield the contract’s mainnet address. The Uniswap pair is deployed by the factory’s CREATE2 and initialized by a constructed run.
All of these are modeled deployments: they run the historical input under current rules and do not prove that the historical transaction was included in the chain. Only the CircuitBreaker, deployed under BPO2, was deployed under rules Jaune covers.
Statements that can fail
Premises that bite.
A premise never needed, or a statement that would survive a change to its code, says less than it seems, so Blanc also proves controls: closed counterexamples, or theorems about every run in which a premise fails.
- For WETH9, a written allowance slot that coincides with a tracked balance slot breaks backing.
- For the EIP-7002 contract, a two-block history that meets every other premise of the request theorem but holds code at the system address violates its conclusion; a stored excess near 2256 makes the bytecode’s bookkeeping depart from the EIP’s recurrence; and a three-block history refutes the EIP’s fee guarantee.
- For the Uniswap pair, the token-answer premise, the callee premises of liveness, the trace-local hash premise, the 112-bit guard and the 32-bit timestamp wrap are each shown to matter; a mint that rounds up, a burn that rounds toward the user, or a different fee constant changes the model’s behavior; and a deployment address one bit off in its salt or init-code hash is a different address.
- For the fixed Vyper pool, three executed witnesses show the exclusion theorem’s antecedent can hold.
- An earlier family of deposit-contract statements assumed that no system contract’s code contains a call- or create-type instruction byte at any offset; Blanc proves that premise false of the canonical EIP-7002 code, and the statements now use the canonical code itself.
The trust base
What the kernel checks, and what it does not.
Axioms. A script walks the dependency graph of every declaration in the library, not only its theorems, from scratch, and fails unless the union of the axioms reached is within Lean’s three standard ones. One walk from all 102,534 constants of the library’s 1,485 modules, auxiliary ones included, visits 130,324 constants and reaches propext, Classical.choice and Quot.sound and nothing else. It covers meta code too. It does not rely on Lean’s #print axioms, which can under-report axioms reached through imported inductive types (an open issue, lean4#15226, about the completeness of that report, not the soundness of the kernel). The walk thereby bounds sorryAx, the axiom behind native evaluation, and any bespoke axiom, for every declaration at once. The same check finds the library’s 1,595 leaf theorems — the results nothing else builds on. The review ledger separately records the last review, and the audit reports new or changed leaves.
Claims. Two gates hold the public account of the results to the code. The claim map for the deployed artifacts must cite names that resolve to declarations at the cited files and lines, recomputes the size and code hash of every artifact from the bytes the repository holds, and must reject each of 25 planted errors. The statement-pin gate restates 1013 statements, each by an example whose type restates a declaration exactly — the headline theorems and the results and definitions their claims are stated through — so weakening any of them fails to elaborate. Neither gate can judge whether a sentence fairly summarizes its theorem; the statements remain the authority.
What the kernel does not check. Two things are trusted: that Jaune’s definitions match Ethereum, which the fixtures support but no theorem can establish — the fixture runs also trusting Lean’s compiler and runtime; and that the lifted bytes are the chain’s, which is recorded provenance, re-checked against three providers at block 26,141,229. Whoever applies a theorem must discharge its hypotheses. The trusted base is small, not minimal: Lean’s kernel, with its arbitrary-precision arithmetic, and Lean’s three standard axioms, all of which the library reaches.
Measured at commit 5048a51f
The cost of checking.
Kernel checking is not free, but it is routine. On the development machine, a 10-core Apple M5 with 24 GiB of memory:
| Check | Scope | Time |
|---|---|---|
| Clean build | the 1,482 modules the library’s root imports, from source, with Blanc’s artifact cache disabled and the toolchain and pinned dependencies prebuilt; wall time, through the host’s memory-admitted build wrapper | 4,380 s |
| Axiom walk and leaf census | 1,484 modules, 128,938 constants, its controls included | 397 s |
| Conformance | 5,006 fixture files at the pinned Jaune revision, one worker | 1,150 s |
| Gate catalogue | 86 rows, every one executed afresh, none reused; all passed | 2,338 s |
The proofs are long compared with the code they describe: WETH9’s 15,221 lines of Lean cover 3,124 bytes, about five lines per byte, and the Uniswap pair’s 95,581 lines cover 11,293 bytes, about eight and a half. The whole library is 725,186 lines in 1,484 modules; the lift of deployed bytecode is 236,372 of them, in 912 files, written by AI agents in fifteen days.
Related work
Neighbors.
Formal verification of Ethereum contracts has explored these trade-offs from many directions, and several projects reach further than Blanc along their own axes. Symbolic tools such as hevm, halmos and the Certora Prover reach bytecode at a scale, and with a degree of automation, that interactive proof does not approach, each approximating Keccak-256 in a documented way. Verified compilers — DeepSEA, Elle, powdr’s Yul compiler, Solidus, Verity — cover the stages they verify; Blanc’s own language belongs to this family. EquiVM is the closest peer along the axis of existing bytecode: it proves that solc and Vyper output refines specifications in a small imperative language, for more than twenty real-world contracts, with whole-interface specifications at a scale Blanc’s bespoke properties do not attempt.
The table below sets the interactive-theorem-proving and K-based systems side by side. Its columns follow this site’s questions and so favor Blanc; each cell describes a project in its own terms, from its documentation, paper or code as read between 1 and 7 October 2026, and “not stated” means its public materials say nothing either way. If a cell short-changes a project, please open an issue; it will be treated as a defect, like an overclaim about Blanc.
| System | Semantics | Existing bytecode | Trust beyond the prover’s standard base, as stated | Gas | Liveness |
|---|---|---|---|---|---|
| Blanc (Lean 4) | Jaune; theorems for Prague, Osaka, BPO1, BPO2 | yes: the mainnet bytes, seven compiler versions and an assembler | none beyond the three standard axioms; recovery a premise of signature-generic theorems; hash separation trace-local, decided or absent, universal on one tier and in one WETH9 statement | exact; closed for WETH9, the Uniswap pair and EIP-7002, explicit sums for the deposit contract, existential for 3Crv | frame, model, reachable state, transaction |
| EquiVM (Lean 4) | EVMLean, a port of EVMYulLean; Cancun | yes: solc and Vyper output, compiled locally from pinned sources | native_decide; two WETH9 return-size axioms (repository); preprint: an opaque Keccak with per-contract selector-hash axioms | not compared; out-of-gas runs excluded | termination “a separate proof obligation” |
| Verifereum (HOL4) | own; Osaka | yes: WETH9’s mainnet bytes | README silent; one cheat, in a lemma used only by commented-out WETH specifications | gas monotonicity theorems (README) | not stated |
| KEVM deposit contract (K) | KEVM | yes: Vyper output; solc 0.6.8 build of a pre-deployment commit | KEVM, the K prover, the bytecode specification | per-function bounds (Solidity version) | deposits accepted given enough gas (Vyper version); success and revert paths (Solidity version) |
| dapp.org, Uniswap V2 (K) | KEVM (2020); fork not stated | yes: bytecode built from the v1.0.0 sources, whose published build matches the deployed runtime | klab’s act implementation, KEVM, the K prover, Z3 and documented lemmas; a token matching the pair’s own assumed | exact symbolic gas for each method’s success | success given at least that gas |
| DeepSEA (Coq) | Hirai’s Lem EVM; fork not named | no | a Keccak injectivity axiom | target uses at most the source’s gas | target succeeds given enough gas; forward simulation |
| powdr (Lean 4) | own relational semantics; Osaka | no | standard axioms only; Keccak opaque with implemented_by; ExternalsRealized hypothesis | existential bound | forward simulation |
| Solidus (Lean 4) | EVMYulLean fork; London to Osaka | no | standard axioms for headline theorems; solc run trusted | gasful refinement; out-of-gas halts allowed; no bound | none claimed |
| Verity (Lean 4) | EVMYulLean fork, native Yul dispatcher; Cancun | no | one axiom on mapping-slot injectivity, per its AXIOMS.md (none in the compiler core, per its README); native_decide; solc trusted from Yul to bytecode | not modeled | none (its paper: correctness does not imply gas-bounded liveness) |
| evm-smith (Lean 4) | EVMYulLean fork, no longer public; SELFDESTRUCT before EIP-6780, per its documentation | no | two axioms; native_decide | tracked; out-of-gas runs vacuous | none (partial correctness) |
Executable EVM semantics are a landscape of their own: KEVM in K, EVMYulLean in Lean, Verifereum’s in HOL4, Isabelle/EVM, powdr’s, and Jaune. Their published conformance figures come from different suites, releases and forks and are not directly comparable.