Blanc, the language.

The whole syntax

Four constructors, and nothing else.

inductive Func : Type
  | branch : Func → Func → Func
  | last : Linst → Func
  | next : Ninst → Func → Func
  | call : Nat → Func

structure Prog : Type where
  (main : Func)
  (aux : List Func)

A Func is a branch on the top of the stack, a terminal instruction, a straight-line instruction followed by more code, or a call into the program’s table of functions — branch, last, next, call. There are no expressions, no variables and no loops as syntax: the instructions are the EVM’s own, and recursion through call and the machine’s stack is all there is, which is exactly what a proof has to walk (Blanc/Semantics.lean).

One liberty of raw bytecode is withheld: computed jump targets. Control flow is the tree you wrote, and the compiler owns every offset. That single restriction is what makes a reusable proof stack possible — inversion tactics that take an execution apart along the program’s own shape, and forward tactics that build one, gas included, without per-contract jump reasoning.

Nothing taken on its word

The compiler is a theorem.

Between a Blanc program and the chain sits exactly one artifact, the compiler, and it enters the theorems rather than the trust base. Its correctness is a backward simulation: every successful EVM execution of the compiled bytes is a run of the source program, so a property proved of the source is a fact about what the EVM executes.

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

For liveness a proof must go the other way and construct an execution. A gas-exact companion relates a run of a compiled program to a successful execution of its bytes in both directions, for programs that do not read their own program counter:

theorem Prog.runCompiled_iff_exec {sevm : Sevm} {pre : Devm} {p : Prog}
    {post : Devm}
    (h_pcf : Prog.pcFree p = true)
    (h_eq : some sevm.code.toList = p.compile) :
    Prog.RunCompiled sevm pre p post ↔ exec ⟨0, sevm, pre⟩ = .ok post

By itself this is not liveness for any contract: it converts run witnesses into executions and back, at the level of one frame. Liveness theorems are built on it, contract by contract.

Why write in it

What writing in Blanc buys.

Reading deployed bytes, Blanc proves what the bytes allow. Writing them, it can also choose bytes that make the proof easier and the contract cheaper. Three dividends recur across the ten contracts.

• Premises designed out. Blanc’s WETH keys balances by raw address words, as above. Its solvency invariant — booked balances, summed over all 2¹⁶⁰ address slots, never exceed the ether the contract holds — is preserved along every configured chain from any state that satisfies it, with no hash premise at all (chainUsing_preserves_solvent). The deployed WETH9’s corresponding results need a premise about the hashed keys a history touches.
• Smaller runtimes, cheaper calls. Six of the seven ports are smaller than the contracts they port, and the seventh, the ERC-4626 vault, is four times larger and still cheaper on every call measured. Two theorems compare Blanc’s WETH with the deployed WETH9 exactly: balanceOf costs 2,260 gas cold against 2,534, and decimals 158 against 2,444.
• Every choice open. Storage layout, dispatch order, calldata handling and error shape are the author’s, down to the instruction — which is how those dividends were designed in rather than argued for.

Sizes are committed artifacts. Except for WETH’s two theorems, the comparisons are finite measurements against a pinned copy of the reference, recorded beside each port in the repository: its manifests, registers and design notes.

Targets you already know

Seven ports.

A port rebuilds a contract that already exists, so every claim can be checked against something a reader already trusts: a frozen statement of the reference’s behavior, a differential corpus run beside the reference’s bytes in a pinned oracle, theorems over the exact compiled Blanc bytes, and a register that publishes every known divergence.

WETH

Wrapped ether after WETH9, in 988 bytes. Solvency — balances summed over every address slot never exceed the ether held — is preserved by every frame, whatever its callees do, and along every configured chain across fork activations, with no hash premise. balanceOf succeeds at exactly 2,260 gas cold, and the composition stratum compares that cost with the deployed WETH9’s by theorem. Its deviation register has five rows. Blanc also verifies the deployed WETH9 itself, a different subject: WETH9.

WETH10

A port of the deployed WETH10 at 0xf4BB…8A9F — all 27 functions and receive, flash loans, ERC-677-style callbacks and EIP-2612 permits — in 6,313 bytes against 9,975. Its flagship is a redeemability guarantee. From a deployment root, which a separate theorem derives from one canonical creation block through Jaune’s block transition, any two legs of valid blocks on Jaune’s mainnet schedule yield, for any holder, an accounted history in which that holder’s booked balance obeys an exact identity in the natural numbers — flash credits and repayments cancel — and every admissible withdraw or withdrawTo up to what remains succeeds with its exact effect, as a message and as a complete signed type-2 transaction (deployment_reachable_future_dualSelector_redeemable_mainnet, statement-pinned; a sibling delivers one history for all holders at once). A generated corpus runs Blanc’s runtime beside the deployed original’s: 147 of 147 rows agree. Its register accepts no behavioral deviation. The deployed WETH10 is the reference here, never the subject: nothing verifies its own bytes.

Beacon deposit contract

The eth2 deposit contract in 2,891 bytes against the deployed 6,358 — 54.5 percent smaller — hashing through the SHA-256 precompile. From a Prague deployment block the proofs themselves reconstruct, every state reachable along a Prague-only schedule, with native SHA-256 admitted at address 0x02, holds a deposit count equal to the length of a deposit list and a root equal to that list’s Merkle root (DeploymentRoot.future_count_root, statement-pinned). Beside the deployed runtime, 44 of 44 differential rows agree, and of 69 runtime transactions 67 are cheaper and 2 equal. Blanc also verifies the deployed contract itself: the deposit contract.

Lido CircuitBreaker

Lido’s pauser registry in 4,282 bytes against 4,584. Registry integrity, as one combined invariant, is preserved along every configured chain over covered forks, with no premise about the code at any other address and none about reentrancy (chainUsing_preserves_registryStable); rooted forms start it from an official-parameters deployment derived through a Prague block. Three registerPauser obligations that Cyfrin’s April 2026 campaign with the Certora Prover left unresolved are corollaries of that invariant, each statement-pinned. 175 of 175 differential rows agree; the register accepts no deviation. Blanc also verifies the deployed CircuitBreaker itself: Lido CircuitBreaker.

Lido withdrawals gateway

The TriggerableWithdrawalsGateway at 0xDC00…037B, the CircuitBreaker’s real pause target: 24 functions and the constructor in 8,094 bytes against 8,128. For every deployment parameter and every distinct CircuitBreaker account, the compiled gateway is a pinned pause target: a clean pauseFor stores exactly the paused-until projection, isPaused answers truthfully, protected functions revert while paused, and no retained write anywhere in a pause’s frame closure touches the CircuitBreaker’s listed cells (pinnedPauseTarget). The differential has 62 agreeing rows and 9 deviating ones, each traced to one of three accepted register entries; two further entries record differences since repaired.

Lido OssifiableProxy

Lido’s upgradeable proxy in 2,188 bytes against 2,497, with delegatecall made a verified capability: for the exact compiled proxy and any delegated child supplied as an execution certificate, the outer message settles to the child’s status, output, logs and the proxy’s storage, gas and warm sets excluded (processMessage_forwardingEnvelope). After a successful ossify, changeAdmin, upgradeTo and ossify end in ProxyIsOssified() from any frame that sees the locked storage, and a separate theorem covers upgradeToAndCall. 85 of 85 differential cases agree; a pre-registered 25-cell efficiency campaign was won 25 to 0; one deviation is accepted.

ERC-4626 vault over WETH

A 25-function share vault over Blanc’s own WETH, ported against OpenZeppelin’s ERC4626 at v5.7.0 — 17,481 bytes against 4,347, four times larger, as its register says, and cheaper on all six measured calls. Its chain-level theorems quantify over two exact compiled contracts at once: from a post-installation checkpoint of the pair, along every configured history, the vault’s shares stay conserved, capped and backed by the WETH the vault holds in WETH’s own ledger, and WETH stays solvent — under one finite, trace-local premise that the allowance keys the history visits do not collide (pair_history_backed); without it, every reachable state is backed or follows an authorized debit. 63 statements are pinned; its register holds nine pre-registered deviations.

Minimal by design

Three études.

An étude is composed from scratch around one hard property, and taken to full proof depth.

FMINT — flash minting

An ERC-3156 flash-mint token in 1,257 bytes. Any well-formed flashLoan call, entered as a fresh non-static frame with at least the stated gas, ends in success, a deliberate revert, or a non-consensus fault — never a consensus exceptional halt — whatever code the borrower runs, with no premise about the borrower (fmint_flashLoan_settles_of_call). That is possible because Jaune’s interpreter is total: the callee’s execution comes from totality, not from an assumption about the callee. Supply conservation, totalSupply = Σ balances, is preserved across arbitrary reentrant borrower code and along every configured chain from any conserved state; totalSupply() costs exactly 2,218 gas.

PRORATA — no profit for any coalition

A pro-rata share ledger with a virtual offset of 1,000, in 343 bytes. Over every realized chain history from a checkpoint where its code is installed with empty storage, in which a victim makes one deposit and at most one full exit, the coalition of everyone else takes out no more than it put in, arbitrary callee code inside the quantifier and no honesty premise anywhere (attacker_no_profit, statement-pinned). An exact-integer brute-force oracle, committed with the family’s first code, had already found that an offset of one leaks one wei in five steps; the no-profit arithmetic was then proved for offsets of at least two.

DRIP — compounding

An accrual-index savings ledger with per-second compounding in 27-decimal fixed point, through a Maker-shaped rpow whose two-sided error band is certified, in 1,762 bytes. Its deployment root is derived from a canonical creation block, and along any configured history, any coalition’s total exits never exceed its principal plus its realized accrual, rounded down — every term a fold over the history’s own calls (history_transcript_entitlement, statement-pinned). No successful drip or join leaves the index stale.

A stratum of its own

Two verified contracts at once.

Contracts are siblings in the import hierarchy: no contract’s module imports another’s, and a gate enforces it. A theorem that genuinely needs two contracts lives in a composition stratum downstream of all of them.

• CircuitBreaker × gateway. At a successful public pause of the CircuitBreaker, with the compiled gateway installed at a distinct, non-precompile target account, the target is left paused at exactly the projection; beyond the ordinary entry premises, nothing is assumed about how the gateway behaves (publicPause_gatewayPinnedTarget); and in two concrete worlds, a finite pause and an infinite one, the successful pause is constructed, not assumed.
• Proxy × two implementations. For an explicit pair of implementations, one authorized execution of the compiled proxy’s upgradeToAndCall, given its initializer child’s run, commits the new implementation and establishes the migration relation, and calls through the proxy are proved to refine before and after.
• Vault × WETH. The backing theorem above, over both contracts’ exact bytes.
• WETH × WETH9. The exact gas comparison of Blanc’s WETH with the deployed WETH9.

The rules

What a port claims.

A port does not claim to be its reference, to the byte; that is a non-goal, permanently. It claims a counterfactual: were the reference being written today, the Blanc implementation would be a better way to build it — behavior that follows a stated, proved specification; an artifact small enough to stay within reach of interactive proof; low-level freedom spent on measured wins. Deviations from the reference are governed, not forbidden: each is a register row with a stance and evidence, and leaving a known divergence unrecorded is the one prohibited move. A port’s theorems are about Blanc’s artifact; where Blanc verifies the deployed original too — WETH9, the deposit contract, the CircuitBreaker — that is a separate subject with its own page. PORTING.md governs.

The fee

What it costs.

A new, deliberately bare language, austere twice over: once to write a contract in four constructors over raw instructions, once to prove it in an interactive theorem prover. There is no Solidity or Vyper syntax, no framework, no library to import beyond what earlier contracts proved, and no auditor already fluent in the source language. For contracts whose invariants are worth more than their development cost — wrappers, vaults, registries, anything whose one job is to keep the books — that trade can be worth making. For code already deployed, it is no longer a trade at all: Blanc reads the bytes that exist.