WETH.

Every theorem above is conditional: it consumes State.Inv at the starting state and returns it at the endpoint. An all-zero ledger satisfies the inequality trivially, and every fixture in the suite installs the committed bytes directly — but no committed theorem states a genesis base case for WETH, and no initcode/CREATE deployment theorem exists on the WETH side. Read the family as exactly what it is: preservation, offered without a rooting theorem. The rooting discipline arrived with WETH10, whose invariants stand on a deployment root derived through the real block pipeline — the standard the portfolio has held itself to since.

Not a covered one. The Using rungs are proved over any configured chain whose schedule selects only covered forks — Prague, Osaka, BPO1, and BPO2 — so an activation among them is one more step of the induction, not a new proof. Beneath them, the fork-parametric parents are stated for an arbitrary covered Fork. A fork outside that list is outside the claim: the pinned Jaune already models Amsterdam, and no WETH theorem covers an Amsterdam block. The unqualified rungs are Prague; nothing on this page implies deployability on earlier forks.

The solvency family is deliberately pure safety, and no prose here inflates it. Liveness is earned separately, where it is actually earned: weth_balanceOf_succeeds and weth_decimals_succeeds construct successful executions instruction by instruction — 2,260 gas cold / 260 warm, and 158, as proved equations — and wethGas_le_max bounds those frames. That is also the honest extent: nothing prices transfer or withdraw, and no transaction-altitude exit theorem exists for WETH. The claim class that closes that gap — redemption proved enabled at every reachable future — is WETH10’s redeemability theorem, not this port’s.

WETH9’s Solidity 0.4.x decoder silently ignores nonzero upper bits in an address word, so a noncanonical alias resolves to the low 160-bit address. Blanc’s mutating paths reject such words outright; the two views use the full word as key material, neither masking nor checking.

The argument: no equivalence claim is made — callers are expected to use canonical ABI encoding, and an alias silently resolving is exactly the kind of implicit behavior a proof-oriented artifact should refuse rather than reproduce. Discharged by a dedicated fixture that probes the dirty word in every position.

WETH9 stores balances in a Solidity mapping, at hash-derived slots. Blanc uses the raw 256-bit address word itself as the storage slot.

The argument: a deliberately simple, proof-oriented representation — storage proofs read off directly, with no hashing lemma in the way. No storage-layout compatibility is claimed anywhere; the same account’s balance simply lives at a different slot, and every fixture in the suite asserts storage at exactly these keys.

Blanc stores an allowance at keccak256(src ‖ dst). In the exceptional case where that hash is also a valid raw-address balance key, approve and allowance-consuming transferFrom revert. WETH9’s domain-separated mapping layout cannot express the collision, so it has no such branch.

The argument: given the simpler layout, the choice is between refusing the operation and silently writing through a third party’s balance slot — and refusing is a feature. The collision branch is untestable by construction (a ~2⁹⁶ search); the registry says so instead of pretending coverage.

WETH9 rejects nonzero call value on every entry point except the payable fallback and deposit(). Blanc originally dispatched on the selector alone: a value-carrying transfer could succeed, the contract kept the ether, and nobody was credited — a permanently unrecoverable surplus.

The resolution: adjudicated under PORTING.md’s then-standing wager (retired 2026-08-19; its policy note records why), value-rejection was ruled a feature by prevailing norms — its modern beneficiary is the buggy integrator, for whom it converts silent permanent loss into a clean revert. Every entry point now carries the shared nonpayable guard: 888 → 988 bytes, 19 gas per guarded call, every priced gas walk re-derived. A fixture shows the suite would have caught the old behavior: rebuilt against the pre-change artifact, 11 of its 21 expectations fail.

The deployed WETH9 runtime contains fourteen REVERT sites and every one is REVERT(0, 0) — empty return data, unused gas handed back. Blanc’s early Func.revert instead reverted over whatever two stack words a guard left live: a garbage-data revert, a stack-underflow halt, or a memory-expansion out-of-gas halt — the latter two burning the frame’s entire gas, which WETH9 never does.

The resolution: Func.revert was normalised to PUSH0 PUSH0 REVERT in the one shared definition, reaching both WETH and FMINT at once — two bytes per revert site, twenty-one sites in the current literal. Against WETH9, which encodes no reason either, the result is agreement; the discriminating fixture evidence lives in the FMINT suite’s falsifier table.