Barely a language. Fully proved.

§ 1 The questions we expect

What a port claims — and how we earn it.

The evidence above is a portfolio of ports: a WETH, a flash-mint token, a full 27-selector WETH10 — contracts you already know, rebuilt in a language you have never heard of. Which invites a fair suspicion: is this claiming to be WETH10 — to the byte? And if not, what kind of win is being advertised?

To the byte: no — permanently no.⁵ What a port claims is a counterfactual: were X being written and deployed today, the Blanc implementation would be a better way to build it — where better is three specific things: behavior that follows a stated, proved specification; an artifact that stays within reach of interactive verification; low-level freedom spent on measured wins. The ports are demonstrations, staged on contracts whose behavior you already know so that the demonstration can be checked against something you trust. And if what you need verified is bytecode already on chain, Blanc is not that instrument — every theorem here is about Blanc’s own artifact, a boundary § 6’s ledger prices with the rest of the bill.

Now grant all of that, and you may still, reasonably, be wondering: what counts as the right behavior — and how do we know the ports have it? This section exists to answer exactly that. A familiar name is not evidence, and a correct compiler is no defense if the program it faithfully compiles is the wrong program. So the answer is built in layers — each catching a different way the claim could fail, none asked to do another’s job. WETH10, the fullest instance to date, answers like this:

Precedent, from the first port: Blanc’s WETH is several times smaller than the deployed WETH9 and cheaper on the call paths measured, and where its simpler storage scheme admits a key-collision WETH9’s layout cannot express, it refuses the operation rather than silently writing through a third party’s balance slot. Each is a deviation from the letter of the reference; each is recorded; and each is a feature no informed deployer would trade back.

§ 2 The language

A blank canvas over the EVM.

Hold the title block’s destination fixed — machine-checked claims about exact deployed bytes, for as wide an X as verification allows — and the language designs itself backwards. Contract languages usually add: types, objects, modifiers, a memory manager, an optimizer pipeline. Every addition is expressive power, and every addition is also distance between what you wrote and what the chain runs. Blanc subtracts instead. The EVM’s own instructions are the vocabulary; four constructors arrange them; the compiler’s one real job is placing jumps. What is left out is the point — the developer keeps the whole surface of the machine, and the verifier keeps a language small enough to prove things about.

The whole grammar, a real endpoint, and the theorem that connects them

-- B·La·N·C.  This is the whole abstract syntax of the
-- language: four constructors over Jaune's instruction
-- types, and a program is functions in a table.
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)

def withdraw : Func :=
  loadCallerBalanceAmount 0 +++ balanceTooSmall +++
  (.call burnBalanceErrorSlot) <?>
  (debitLoadedBalance +++
    caller ::: arg 0 +++ pushB256 0 ::: emitTransfer +++
    swap 0 ::: pop :::
    sendValueToCaller +++ iszero :::
    (.call ethTransferErrorSlot) <?>
    Func.stop)

-- Backward simulation: from any successful EVM execution
-- of the compiled bytes, recover a source-level run.
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

-- And, gas-exact, in both directions — the bridge that
-- lets a proof construct a real execution, not just
-- take one apart.
theorem Prog.runCompiled_iff_exec …
    Prog.RunCompiled sevm pre p post ↔ exec ⟨0, sevm, pre⟩ = .ok post

§ 3 The portfolio

Three contracts in.

Each contract raised the bar for the next: WETH established the method, FMINT added adversarial callbacks and made the shared-module discipline load-bearing, and WETH10 — a full 27-selector production surface with flash mints, ERC-677-style callbacks, and EIP-2612 permit — is the demonstration that the method scales.

Table 1 — the current portfolio. Sizes are committed literals checked by gates (check-runtime-bytes.py compares every fixture’s installed code byte-for-byte against the Lean literal); the deployed WETH9 and WETH10 figures come from the pinned reference locks in the deviation registries. Smaller is not the pitch — proved is — but the sizes fall out of a language with no mandatory dispatcher or ABI scaffolding, and they are measured, not asserted.

Contracts are siblings in the import hierarchy — no contract’s module imports another’s, mechanically enforced by a layering gate. When one contract needs something another defined, that is evidence the thing was never contract-specific, and it moves upstream with a rename. The shared layer this discipline has accreted — the verification ladder, forward and inversion tactic families, the callback-crossing machinery — is the real asset: it is why the third contract cost a day, not a season.

§ 4 The flagship

What a holder is promised: future redeemability.

Wrapped ether has one job: a booked balance must be a claim on real ETH that its holder can actually collect. Most verification stops at an invariant — “the books balance now.” The flagship, landed 2026-08-12, goes where the user’s risk actually lives: any reachable future, after arbitrary other actors — flash loans, reentrancy, hostile callbacks — have done their worst.

theorem deployment_reachable_future_dualSelector_redeemable
    {chainId : UInt64} {dp : DeployParams} {ca u : Adr}
    {base deployed checkpoint future : BlockChain}
    (hroot : Weth10.DeploymentRoot chainId base deployed dp ca)
    (hcheckpoint : BlockChain.ReachUsing (ChainConfig.pragueOnly chainId) deployed checkpoint)
    (hfuture : BlockChain.ReachUsing (ChainConfig.pragueOnly chainId) checkpoint future) :
    ∃ history, FutureDualSelectorRedemptionGuarantee
      chainId dp ca u checkpoint future history

Read the quantifiers — u is every holder, not a specially chosen one. This dual-selector theorem is pointwise. Its sibling deployment_reachable_future_redeemable_allHolders packages one history carrying the inherited FutureRedemptionGuarantee for all holders at once; it does not claim a dual-selector all-holders package. ReachUsing is Jaune’s configured-chain reachability: whole valid blocks, every transaction anyone sent, arbitrary contracts doing arbitrary things — under the model’s one global side condition, that total ETH plus pending withdrawals stays below 2²⁵⁶ wei. The history is obtained from the reachability derivation, not reconstructed from the endpoints — a logical guarantee about the window, not a trace extractor. And the deployment root is no opaque axiom: given one successful canonical creation-block transition through Jaune’s actual Prague block pipeline, DeploymentRoot — receipt success, exact installed runtime, empty storage — is derived, not assumed.

The guarantee, field by field

bookedBalanceNat deployed.state ca u
    ≤ bookedBalanceNat future.state ca u

§ 5 Breadth

Theorems most stacks cannot state.

The flagship is one theorem. The claim behind it is a capability: because contracts, compiler, and chain semantics are one mathematical object, statements that fall outside other tools’ vocabularies are ordinary here. Six kinds, each with a landed instance you can open.

Each panel names its theorem; the statements — with their premises, which are part of the claim — are the authority. Where a family is partial correctness, the repository says so in the module docstring; where nothing says a call succeeds, no page of prose may imply one does.

§ 6 Candour

The price, unvarnished.

Everything above is bought, not free, and the bill is itemisable. Blanc is a steep ask and not for everyone — the pitch is not that the price is small, but that what it buys is not sold elsewhere.

Who should not use Blanc: teams iterating on product-market fit, systems built around upgradeable proxies and vendored library ecosystems, and anyone whose assurance story must be legible to today’s audit market. Who plausibly should: contracts whose invariants are worth more than their development cost — bridges, wrappers, vaults, anything whose one job is to never lose the books. For that class, the next section is the part of the bill that changed.

§ 7 The bill, revised

What agents change — with receipts.

The traditional objection to interactive verification is not doubt about the theorems; it is the invoice — expert-months per contract. That number was measured this month, on this repository, and it is no longer what people remember it being.

An honest velocity claim needs an honest denominator: 21 hours bought WETH10’s charter — implementation, endpoint theorems, deployment, differential evidence. The flagship of § 4 was a successor program, landed over the following three days by the same method. The unit economics — days per verified contract, tokens in dollars — are the differentiator this project intends to keep publishing, run by run.

§ 8 Position

The penultimate form.

Blanc agrees with the direction — and adds one amendment from practice.

If machine code written and proved by machines is the final form of software development, Blanc is a considered bid for the penultimate one — and for contracts holding other people’s money, the penultimate form may be the right place to stop.

§ 9 Who this is for

Three ways in.

§ 10 Reproduce it

One clone, a build, and the audit.

The only prerequisite is elan, the Lean toolchain manager. Blanc pins Jaune by immutable commit in its lakefile, so a fresh clone builds reproducibly with no sibling checkout — and “which semantics was this proved against” has a one-line answer.