A minimal EVM contract language · Lean 4

Keep every freedom.
Except one.

Freedom from trusted compilers, proving theorems about the exact bytes that deploy; freedom to check every proof yourself, with a small kernel, three classical axioms, and nothing else; freedom from semantic gaps with mainnet, built on an executable EVM semantics passing the ecosystem’s own fixture corpus in full, 5,006/5,006 supported files; freedom to write custom, hand-optimized bytecode down to the last instruction, jumps alone placed by the proved compiler; and the freedom of expressing and proving any property, up to liveness constructed over every reachable future — a ceiling rarely available at any price.¹

The bill is one line: a new, deliberately bare language, austere to write and austere to prove in. § 1–6 are what you keep. § 7 is the language you pay it in; § 8, the bill; § 6, the receipts.

What you keep — § 1–6 What you pay — § 7–8

$ lake build $ scripts/check.sh --no-build OK — axiom audit: one union walk over Blanc reaches only the standard axioms; 2247 leaf results $ scripts/check-weth10-differential.sh OK — WETH10 differential: 147/147 rows agree; 28 runtime entries (27 selectors + receive), 2 identity worlds …

Fig. 1 — two of the repository’s gates: the axiom-audit line is that gate’s verdict wording at the current audited inventory, which a static gate derives from the committed audit file; the WETH10 differential line is verbatim from the exact-candidate run of 2026-09-03 UTC. The gates pin every audited theorem to its exact axiom set and execute Blanc’s WETH10 beside the deployed original’s runtime, byte for byte, in a pinned oracle.³

0 sorry — CI-enforced axioms: propext · choice · quot 2247 leaf results, one axiom walk in CI Jaune pinned by commit

Abstract. Blanc is a contract language for the Ethereum Virtual Machine that adds as little to the machine as its authors could manage — four constructors over the raw instruction set, a compiler into deployable bytecode, and a machine-checked proof that the compiler is correct — and asks its user to give up as little: theorems land on the exact bytes that deploy; every declaration is walked for axioms in CI, within Lean’s three canonical axioms; and the semantics underneath, Jaune, is executable and passes the ecosystem’s own fixture corpus. Ten contracts are in — seven ports and three études, each with a page of receipts — among them a WETH10 whose every holder is proved able to redeem at every reachable future of a proved deployment, Lido’s CircuitBreaker with its Registry integrity carried from an official-parameters deployment to every reachable state, and the eth2 deposit contract, its Merkle root carried through twelve SHA-256 precompile crossings to every admitted future. Each port is defended in layers — a frozen behavior contract, a differential corpus beside the deployed reference, theorems over the exact compiled bytes, a deviation registry that publishes every known divergence before anyone asks — and one port, the ERC-4626 vault, is four times the size of its reference and says so in its registry, beside the gas it saves on every measured call. The fee is one line, and this page never pretends it is small: a new, deliberately bare language, austere to write and austere to prove in. MIT-licensed.

4 constructors in the whole language — branch, last, next, call. The name is the syntax

2247 leaf results — independently valuable theorems, all axiom-checked by one walk of the whole library, in CI on every commit

10 contracts in — seven ports, three études, from a WETH to the eth2 deposit contract — each with a page of receipts

147/147 differential rows agreeing with the deployed WETH10 — all 27 selectors + receive, zero mismatches

§ 1 What you keep

Keep the bytes.

Every contract theorem on this page is about the exact runtime bytes that deploy — not about a source file a trusted toolchain will later turn into something else. Between your program and the chain sits exactly one added artifact, the compiler, and it enters the theorems rather than the trust base: its correctness is itself a machine-checked theorem, proved once, inherited by every contract, and nothing is taken on its word.

Blanc/CommonCore.lean · Blanc/Compiled.leancompiler correctness

-- 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

The direction of correct matters: a property proved of the source is thereby a fact about what the EVM executes. The biconditional adds the forward direction, which is what liveness and exact-gas theorems are built on.

what lands on the bytes

Everything downstream is stated at this altitude. The property inventory of § 5 and the endpoint families of § 9 hypothesise the compiled bytes in so many words — some sevm.code.toList = p.compile is a premise found inside the statements, not a convention explained beside them. Even deployment stays on the bytes: WETH10’s root is derived through the real creation-block pipeline — receipt, installed runtime, and all.

What the machine itself does is not Blanc’s to say. That ground — and the evidence it stands on — is § 3. The language the bytes are written in — and what it costs — is § 7.

§ 2 What you keep

Keep the standard of proof.

A verification result is worth what it costs to doubt. Doubting one of Blanc’s costs a lot: every claim is a Lean theorem with a proof object, and the checker of record is Lean’s small kernel — not this project’s code, not a search procedure’s verdict, not a report you are asked to take on reputation. Checking it again yourself is a command, not a negotiation.

the trust base, exhaustively

Three axioms at most, no oracle. One from-scratch walk in CI follows every constant of the library, and fails unless the union of the axioms it reaches is drawn from propext, Classical.choice, and Quot.sound — Lean’s three canonical axioms, the same ground ordinary classical mathematics stands on. The audit fails on any other axiom, on sorryAx, and on any native_decide-style escape into compiled evaluation. Nothing out-of-kernel stands between a statement and its checking.

statements pinned, not just proofs

A weakened conclusion fails as loudly as a broken proof. Proving something is cheap; the discipline is keeping the something fixed. A statement-pin gate Lean-checks the exact wording of the protected claims — 460 definitions, statements, and record constructors across the shared layer and the protected contract families — so the theorem quoted on this page is character-for-character the theorem CI checks, and a quiet regression in what is claimed trips the same wire as a regression in whether it holds.

One consequence, bought early and spent in § 6: this standard is indifferent to authorship. A proof written by an agent is checked by the same kernel against the same pinned axioms as a proof written by hand — the trust never lived in the author.

§ 3 What you keep

Keep the ground under the theorems.

A contract theorem means no more than the machine model it quantifies over. Blanc states nothing about the EVM on its own authority: every theorem bottoms out in Jaune — an executable EVM semantics written in plain Lean 4, imported at a pinned immutable commit — so “which semantics was this proved against” always has a one-line answer.

a semantics that runs

Believing it is not an act of reading. Because the semantics executes, it can be tested like an implementation: at the pinned commit it passes the ecosystem’s mainnet fixture corpus in full — 5,006/5,006 supported files — and Blanc’s differential gates run each contract in a pinned oracle, beside EELS, Ethereum’s canonical executable specification, or through the pinned Jaune’s own t8n: 147/147 WETH10 rows, 175/175 CircuitBreaker rows, 85/85 OssifiableProxy rows, 44/44 deposit-contract rows, 62 agreements plus 9 registered deviations for the withdrawals gateway, all 25 selectors of the ERC-4626 vault beside its compiled OpenZeppelin reference, 11/11, 11/11, and 14/14 fixture suites, and DRIP’s 91 committed BPO2 fixtures. The definitions the corpus exercises are the definitions the theorems quantify over — one set, no shadow model.

the fine print, kept fine

Separate trust stories, kept separate. Corpus runs go through Lean’s compiled evaluation; the theorems never rest on that run — their checking is § 2’s kernel, end to end. The interpreter is total, which is what lets § 5 prove settlement theorems with no premise about a hostile callee. And no theorem is quietly relative to an unstated protocol version: each names its chain configuration in its own premises — ChainConfig.pragueOnly, fork schedules crossing Prague through BPO2 — and every frame or schedule it quantifies over is confined to the four forks its proofs cover, CoveredFork: Prague, Osaka, BPO1, BPO2. So what was proved, and against what, lives in the statement rather than in a changelog.

The division of labour is exact — Jaune owns what the machine does; Blanc owns programs, the compiler, and everything proved about particular contracts — and Jaune keeps an evidence page of its own.

§ 4 What you keep

Keep the whole design space.

Storage schemes, stack discipline, dispatch order, calldata handling, error genre, gas layout: every implementation decision is yours, down to the instruction. That freedom is not an aesthetic. It is where whole classes of hypothesis, byte, and gas get designed out before anyone has to argue them away — and each dividend below is either proved or measured, never projected.

hypotheses, designed out

Solvency with no collision clause

Blanc’s WETH keeps its ledger at raw address words — a scheme a hashed mapping layout cannot express. Its solvency theorem therefore carries no hash-injectivity hypothesis, no “assuming no collisions this transaction”: the statement holds in every case, full stop, because the implementation never bet on a hash. And where the scheme admits a collision the reference cannot express, the contract refuses the write rather than writing through a third party’s balance slot.

bytes, spent well

Small enough to prove, lean enough to run

988 bytes of WETH runtime against the deployed WETH9’s 3,124; 6,313 of WETH10 against 9,975, with all 27 selectors kept. The same austerity that shrinks the artifact is what holds it within reach of interactive proof — and the measured call-path deltas live on each contract’s page, beside its deviations.

cost, made exact

Discipline you choose, numbers you prove

Error genre is a decision, not an accident: every revert site compiles to PUSH0 PUSH0 REVERT, one observable shape. Dispatch order and calldata handling are decisions too. And because the artifact is fixed and structured, per-endpoint gas closes into proved equations rather than profiler estimates — § 5 shows them, cold and warm.

One liberty is withheld — computed jump targets, the single structural trade § 7 spells out. Everything else about the artifact is yours to decide, which is the difference between a language that permits optimization and a language that merely tolerates it.

§ 5 What you keep

Keep the ceiling.

Because contracts, compiler, and chain semantics are one mathematical object, statements of a kind rarely available at any price are ordinary here. Eleven kinds have landed so far, each with an instance you can open.

Liveness, constructed, over every reachable future.

Safety’s neglected dual: “the contract cannot lose your money” is only half a promise — “and it will actually give it back” is the other half. Small instances are routine here: weth_balanceOf_succeeds and its family build a successful execution instruction by instruction, exact gas in the statement. The kind is stated in full by WETH10’s redeemability guarantee (2026-08-12), where a holder’s risk actually lives: at any reachable future of a proved deployment, after arbitrary other actors — flash loans, reentrancy, hostile callbacks — have done their worst.

machine-checked

Theorem (deployment_reachable_future_dualSelector_redeemable_mainnet, Blanc/Weth10Mainnet.lean).

From a proved deployment of the exact compiled WETH10 runtime, any leg of valid blocks selected by Jaune’s configured mainnet schedule to a checkpoint, and any further configured leg to an arbitrary future snapshot, there is an accounted history of the window carrying the dual-selector redemption guarantee below for an arbitrary holder u. The unsuffixed theorem has the same shape for any cfg whose schedule selects only covered forks.

theorem deployment_reachable_future_dualSelector_redeemable_mainnet
    {dp : DeployParams} {ca u : Adr}
    {base deployed checkpoint future : BlockChain}
    (hroot : MainnetDeploymentRoot base deployed dp ca)
    (hcheckpoint : BlockChain.ReachUsing mainnetChainConfig deployed checkpoint)
    (hfuture : BlockChain.ReachUsing mainnetChainConfig checkpoint future) :
    ∃ history, FutureDualSelectorRedemptionGuarantee
      mainnetChainConfig dp ca u checkpoint future history

Read the quantifiers — u is every holder, not a specially chosen one. 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. The deployment root is no opaque axiom: from one successful canonical creation-block transition through Jaune’s selected configured rules, DeploymentRoot cfg — receipt success, exact installed runtime, empty storage — is derived, not assumed. The public mainnet constructor selects BPO2. And an all-holders sibling delivers one history carrying the guarantee for every holder at once, without the dual-selector packaging.

what the guarantee packages

Books that balance in ℕ. B₀ + ordinaryIn = Bₜ + redeemed + externalTransferredOut — flash-mint credits and repayments proved to pair exactly and cancel, committed credits proved not to wrap, no hidden modular slack. Hence the floor B₀ ≤ Bₜ + redeemed + externalTransferredOut: whatever the window did, it cannot dilute a holder below their residual.

Exits that provably open, at two altitudes. For every amount within the residual, every admissible canonical withdraw or withdrawTo message at the future snapshot succeeds — constructed execution, not absence of counterexample — and so does the complete signed type-2 transaction, intrinsic gas, validity, and settlement included. For a funded code-free external holder with canonical fields, recovery of its own signature is the sole unproved input.

Attribution, and two corollaries. Under one stated hash hypothesis, every nonzero permanent outflow in the deployment window traces to the holder’s own call, its in-window approve, or its in-window permit — only attribution takes that hypothesis; redeemability never does. Downstream sit the dormant holder — no effectful authorizing act, not a wei lost — and any-order redemption over any supplied duplicate-free holder list, the bank-run shape, with the aggregate effect on balances and ETH exact.

where it stops

The subject is the exact compiled Blanc runtime on an explicit configured schedule, from its proved deployment root — never the Solidity artifact deployed at 0xf4BB…8A9F, which nothing here verifies. Attribution names the account whose recorded act the runtime accepted, not consent or intent: a phished approve and a relayed permit both attribute to the signing account. Redemption theorems consume the holder’s message or signed transaction as an input; no theorem forges a signature. A holder with non-delegation contract code that cannot call WETH10 keeps a conserved balance but has no transaction-altitude exit of its own. The supplied everyone-list is not a state enumeration. Inclusion, propagation, key custody, and fee markets are out of frame. The full boundary lives in PORTING.md and the WETH10 registries — declared non-claims, in the honest register.

WETH10’s mainnet schedule is exact: Prague at Unix 1746612311, Osaka at 1764798551, BPO1 at 1765290071, and BPO2 at 1767747671; BPO2 has been live on mainnet since 2026-01-07. A later fork that changes only rule data Jaune already models is a pin bump and re-verification with any new facts explicit. A fork that changes execution semantics changes Jaune itself, and that has now happened once: the pinned Jaune models Amsterdam — its gas metering and block-level access lists — while every Blanc theorem stays confined to Prague, Osaka, BPO1, and BPO2. No Blanc result covers an Amsterdam frame or block.

Ten more kinds — still uncommon

adversarial settlement

No premise about the borrower

fmint_flashLoan_settles: a funded, non-static flashLoan frame ends in success, a deliberate revert, or the non-consensus fault channel — never a consensus exceptional halt — with the borrower’s code universally quantified. Possible because Jaune’s interpreter is total: the callee’s execution comes from totality, not from an assumption about the callee.

chain altitude

Invariants that survive hard forks

WETH solvency and FMINT conservation are preserved over every state reachable along a valid configured chain — induction over whole blocks, withdrawals and system operations included, across scheduled fork activations from Prague through BPO2. A protocol upgrade is a step in the induction, not a threat to the claim.

gas, closed-form

The gas cost is a theorem

fmint.totalSupply() costs 2,218 gas — exactly, as a proved equation, not a profiler’s estimate. WETH’s balanceOf: 2,260 cold, with the 19-gas nonpayable guard visible in the statement. WETH10’s required views carry exact cold/warm gas uniformly over deployment parameters. Closed forms and maxima ship as lemmas beside the code.

deployment

Creation, through the real pipeline

WETH10’s deployment root is derived, not axiomatized: from one successful strict singleton type-2 creation block through Jaune’s selected configured transition, the proof reconstructs receipt success, exact installed runtime, empty storage, and the crossed request-system calls — establishing the DeploymentRoot the guarantee above stands on, with the creation message’s 1,264,071-gas cost as a closed form. The public current-mainnet root is witnessed by a committed BPO2 block and replayed through Jaune; the Prague form remains a corollary.

open-contract histories

Integrity with no premise about anyone else

chainUsing_preserves_registryStable: from a checkpoint with the CircuitBreaker’s exact runtime installed and coherent storage, every reachable state stays coherent — with no premise about the bytecode at any other address, no non-reentrancy condition, and no honesty asked of the contracts it pauses. The checkpoint hypothesis is discharged by a proved official-parameters deployment, so the family stands on a derived deployment root rather than an assumed checkpoint.

error genre

Reverts, constructed exactly

Not “no success exists” but this call reverts, with this error, and no data: unknown-selector and guard executions built instruction by instruction to .error (.revert, _) with empty returndata. Every Blanc revert site is PUSH0 PUSH0 REVERT — a discipline a fixture falsifier table shows is observably distinct from the three failure shapes it replaced.

adversarial arithmetic

No profit, with no honesty premise

attacker_no_profit: over any attack trace realized along a configured chain from PRORATA’s deployment root — a coalition’s deposits, withdrawals, and donations interleaved around a victim’s deposit — the coalition takes out no more than it put in, with arbitrary callee code inside the quantifier and the 2 ≤ O the pure result needs discharged from the compiled offset. The offset-one leak was found by brute force before any proof was attempted.

precompile crossings

A Merkle root through the SHA-256 precompile

The deposit contract hashes by STATICCALL to address 0x2 at twelve source-shaped sites; the proofs name the fork’s precompile selection, prove the 64-byte input, and instantiate the answer as exactly Bytes.sha256 — environment facts, not a hash axiom. From a derived Prague deployment, DeploymentRoot.future_count_root reads the exact count and mixed root off every admitted future.

delegation, owned

An upgrade that is really a migration

Code address and storage owner pulled apart: a forwarding envelope for an arbitrary certified child, and upgradeToAndCall_primary_realizes_migration — one authorized execution of the exact compiled OssifiableProxy commits v2, runs the initializer child it spawns, and establishes the relation R2, with calls through the proxy proved to refine before and after. Migration soundness and behavioral refinement are separate conclusions, never evidence for each other.

composition

Two verified contracts at once

publicPause_gatewayPinnedTarget: at a successful public pause of the CircuitBreaker with the exact compiled withdrawals gateway installed at the target, the gateway is left paused at exactly the shared projection and the CircuitBreaker’s own cells are untouched — noninterference discharged, not assumed, and no code-shape premise at all. And the run is no longer a premise: gatewayPauseWorld_closedPublicPause and its sentinel sibling construct it in two concrete Prague worlds, a finite and an infinite pause.

Each entry 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 What you keep

Keep the receipts.

The freedoms above are not a prospectus. Every contract theorem, differential row, and measured byte in § 1–5 comes from one of ten contracts already in. Each contract raised the bar for the next, and each has a page of its own: how we know it is the contract it names, the deviation registry, the measured deltas, and what the build taught. Three kinds are kept distinct. Ports target a contract that already exists, so every claim can be checked against something you already trust. Études are composed from scratch — deliberately bare contracts, each written to push one hard capability to full proof depth. Compositions are theorems about two verified contracts at once, and live in a stratum of the repository that neither contract may import.

Ports — targets you already know

WETHwrapped ether · after WETH9

The first port, and the method’s proof of concept: solvency — the contract always holds enough ETH to honour every balance — carried from a single frame up to every reachable state of a configured chain, across scheduled fork activations.

988 B vs 3,124 deployed solvency at chain altitude 11 oracle fixtures evidence · deviations · deltas · notes→ WETH10flash-minting wrapped ether · after the deployed WETH10

All 27 selectors plus receive, flash loans, ERC-677-style callbacks, EIP-2612 permit — zero contract code to a closed verification charter, and the future-redeemability theorem of § 5 on top.

6,313 B vs 9,975 deployed 147/147 differential rows 28/28 entry families proved evidence · deviations · deltas · notes→ CircuitBreakerLido’s emergency pause guardian · after the deployed CircuitBreaker

Registry integrity as one combined invariant — its corollaries close the three obligations an industrial campaign left open — rooted in a proved official-parameters deployment through the full Prague block pipeline, and preserved at every reachable future over arbitrary hostile callees.

4,282 B vs 4,584 deployed 175/175 differential rows 0 accepted deviations evidence · deviations · deltas · notes→ BeaconDepositthe eth2 deposit contract · after the deployed original

The incremental Merkle accumulator proved from a hash-parametric model down to the exact bytes — across twelve SHA-256 precompile crossings — rooted in a derived Prague deployment, with the exact count and mixed root read off every admitted future.

2,891 B vs 6,358 deployed 44/44 rows · 0 dearer paths 30-declaration register evidence · deviations · deltas · notes→ TriggerableWithdrawalsGatewayLido’s exit gateway · after the deployed gateway

The CircuitBreaker’s real pause target: 24 selectors and the constructor, the pinned-pause-target bundle proved with noninterference discharged rather than assumed — once the portfolio’s one larger, dearer port, now smaller than its reference and cheaper on all 51 measured paths.

8,094 B vs 8,128 deployed 62 + 9 differential rows 3 accepted · 2 repaired evidence · deviations · deltas · notes→ OssifiableProxyLido’s upgradeable proxy · after the deployed proxy

Delegatecall made a verified capability: a forwarding envelope for an arbitrary child, all seven control entries with ossification proved irreversible, whole-CREATE rollback, a pre-registered 25-cell efficiency campaign won 25 to 0 — and an upgrade proved to realize its migration.

2,188 B vs 2,497 deployed 85/85 rows · 25/25 gas wins 1 accepted deviation evidence · deviations · deltas · notes→ ERC-4626 vaulta share vault over WETH · after OpenZeppelin’s ERC4626

All 25 functions with exact compiled effects over Blanc’s own WETH, capacity proved honest as a statement about why a call can revert, and backing, exact rounding residue, and no coalition profit carried along every configured history of the vault–WETH pair.

17,481 B vs 4,347 reference cheaper on 6 of 6 measured calls 9 pre-registered deviations evidence · deviations · deltas · notes→

Études — minimal by design

FMINTERC-3156 flash-mint token · referenced against OpenZeppelin

A token pared down to the one hard thing flash minting adds: supply conservation — totalSupply = Σ balances — proved under arbitrary reentrant borrower code, with a settlement trichotomy carrying no premise about the borrower at all.

1,257 B runtime conservation vs any borrower 11 fixtures / 188 assertions evidence · deviations · deltas · notes→ PRORATApro-rata share ledger · étude #2 of the arithmetic série

Ratio pricing as an adversarial surface: rounding direction, zero-tolerance preview/actual consistency, and cumulative dust conserved along every configured history — and the inflation attack proved impossible with no honesty premise on any callee, its offset-one leak found by brute force first.

343 B runtime no profit vs any coalition 14 fixtures / 131 assertions evidence · oracle · deltas · notes→ DRIPaccrual-index savings ledger · étude #3

Compounding as fixed-point arithmetic: a Maker-shaped rpow with a certified two-sided error band, a stale index proved impossible after every successful call, and exact books for every join, drip, and exit along each configured history.

1,762 B runtime certified rpow band 91 fixtures / 137 transactions evidence · oracle · deltas · notes→

Compositions — two verified contracts at once

CircuitBreaker × Gatewaya pause that leaves its target paused

The first inhabitant of the composition stratum: at a successful public pause of the CircuitBreaker with the exact compiled gateway installed at the target, the gateway is left paused at the shared projection and the CircuitBreaker’s cells are preserved — no code-shape premise, noninterference discharged — and two concrete worlds in which that successful pause is constructed, not assumed.

12 audited theorems no code-shape premise 2 closed worlds theorem · controls · boundary→ Proxy × two implementationsupgrade equivalence, as a theorem

Five explicit objects — proxy, v1, v2, migration, relation — and two conclusions kept apart: the migration is sound for R2, and the exact compiled proxy’s upgradeToAndCall performs it, with calls through the proxy proved to refine before and after. Twelve executable rows pinned byte for byte.

10 headlines · 3 assurance theorems 12 witness rows 45 self-test controls theorem · witnesses · boundary→ Vault × WETHa vault that proves its own asset

The vault’s chain-level theorems quantify over two exact compiled contracts at once: every WETH frame that touches the vault’s row is classified, and under one finite, stated key-noncollision premise the pair stays backed and WETH stays solvent at every configured state it reaches.

34 composition modules 3 exact child forms 1 premise, named theorems · premise · boundary→

One goal from WETH10’s committed charter did not land, and the ledger says so: a settlement theorem carried over from the previous contract turned out to be false of WETH10’s design. It was struck by explicit amendment, with no replacement installed and nothing nearby relabeled to fill the row. Striking a false goal is the system working — a project that never records a lost bet is not reporting, it is advertising. The same ledgers record that the vault port is four times its reference’s size, and that its attack-trace inhabitant is model-level only: no executed history meeting the attack premises is exhibited.

why the trust story is unchanged

Agent-written proofs are exactly as trustworthy as human-written ones, because the trust never lived in the author: every proof, whoever wrote it, is checked by Lean’s kernel, and every audited theorem’s axiom closure is pinned in CI. The gates are built to be hostile to wishful reporting — falsifiers that must fail, shrink-only budgets, coverage that refuses credit for a selector merely embedded in bytes.

The human stayed where judgment lives: adjudicating conformance questions, striking the false goal, deciding what a port owes its users. The agent did the part that scales.

$ scripts/check-layering.sh OK — layering: 10 contract(s) are siblings; 496 module(s) classified, 494 non-root checked, 40 composition module(s) downstream, no cross-contract, inverted or composition-inverted import; … $ scripts/check-claims.sh OK — claim statements: 460 definitions/statements and exact record constructors pinned by Lean $ scripts/check-weth.sh --no-build && scripts/check-fmint.sh --no-build OK — weth fixtures: 11/11 PASS OK — fmint fixtures: 11/11 PASS, manifest cross-check clean

Fig. 2 — the fast half of the gate battery. The layering line is verbatim from a run on 2026-09-25 UTC, ellipsis marking its two trailing registry clauses; the fixture lines are verbatim from the exact-candidate run of 2026-09-03 UTC; the claim line is that gate’s own verdict wording at the current pin count, which a static gate derives from the committed pin file. The full ordered set — layering, trust surface, reference lock, differential, redemption, deployment, axiom audit, statement pins, elaboration budget, fixtures, coverage — is catalogued with scales and pass criteria in scripts/GATES.md.

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, the retained execution carriers an étude built to carry its accounting — is the asset each next contract inherits whole. A theorem that genuinely needs two families — a CircuitBreaker pausing a gateway, a vault holding WETH — has one home: a composition stratum strictly downstream of every contract, which no contract or shared module may import. A contract joins the portfolio when its registers close.

§ 7 What you pay

Barely a language.

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 — distance that ends up paid for in trust. Blanc subtracts instead. The EVM’s own instructions are the vocabulary; four constructors — branch, last, next, call: they spell the name, and they are the whole language — 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.

7.1 — the name is the syntax

Four constructors, no fifth

A Func is a branch on the stack top, a straight-line next, a terminal last, or a call into the program’s function table. There are no expressions, no variables, no loops-as-syntax — recursion through call and the machine’s own stack are all there is, which is exactly what a proof has to walk.

7.2 — structure where it pays

The one liberty withheld

Raw bytecode lets a program compute a jump target from anything. Blanc doesn’t: 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 account included, without per-contract jump reasoning.

7.3 — batteries, written and proved

The library is whatever you prove

No standard library comes along to be trusted either: what exists today is what ten contracts have needed — a dispatcher pattern, ABI helpers, a shared nonpayable guard, a proof ladder — each an ordinary Lean definition, written once, proved, and reused by the next contract. § 8 prices what the austerity costs; § 4 measured what it buys.

The whole grammar, and a real endpoint

Blanc/Semantics.leanthe entire syntax

-- 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)

Blanc/Weth10.leansource

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

Instructions are the EVM’s own; ::: is next, <?> is branch, and every name above it is ordinary Lean definition — the “standard library” is whatever you prove you need.

Four constructors is a position, not a shortage — § 10 defends it, one step up from the obvious alternative of none at all.

§ 8 What you pay

The fee, unvarnished.

Everything § 1–6 keeps is bought with a single purchase — the language above: new, deliberately bare, austere twice over — once to write your contract in four constructors, once to prove it in an interactive theorem prover. One line on the bill; this section itemises it. The pitch was never that the fee is small — it is that what it buys is not sold elsewhere, and that nothing else is on the bill.

the ledger — four facets of the fee, and one boundary

Solidity, Vyper, and their ecosystems no familiar syntax, no IDE plugins, no framework integration, no OpenZeppelin to import, no auditor fluent in your source language
gone
Batteries not included: the standard library is what ten contracts have needed so far — what your contract needs beyond it, you write, and then you prove
not included
Distance from the machine Blanc code is EVM instructions with four combinators; you think about the stack, storage words, and gas — the language will not think about them for you
by design
Proof effort that rounds to zero the theorems above sit in a library of ~490,000 lines of Lean; interactive proof is real engineering, even with the shared ladder doing the heavy lifting
real cost
Verification of contracts already deployed not a fee but a boundary: the theorems are about Blanc’s artifact — verifying the original at its address is a different project, worth doing, and not this one
out of scope

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, § 6 holds the receipts.

§ 9 The questions we expect

What a port claims — and how we earn it.

The portfolio of § 6 is staged on contracts you already know — a WETH, a full 27-selector WETH10, the eth2 deposit contract, Lido’s CircuitBreaker, its withdrawals gateway, and its upgradeable proxy, and OpenZeppelin’s ERC-4626 vault over WETH — 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. 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 § 8’s ledger prices with the rest of the bill.

Grant all of that, and a harder question is still open: what counts as the right behavior — and how do we know the ports have it? 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 answers like this:

the statement

WETH10_COMPATIBILITY.md

“Right” is written down before it is argued. A compatibility contract freezes the reference’s ordinary-call public boundary, endpoint by endpoint — all 27 selectors and receive: outputs, state and ETH effects, logs, guard order, rollback, what a callback may observe mid-flight — and every row names the evidence that owns it. A behavior nowhere stated can be neither checked nor falsified, so the statement comes first, and it is committed.

the sanity check

check-weth10-differential.sh

The cheapest way to be wrong is to prove the wrong program — tests catch that first. A generated corpus executes Blanc’s exact runtime beside the deployed original’s, byte for byte, in a pinned oracle: 147 rows across every entry, two identity worlds, hostile reentrancy, static contexts, eight live channel falsifiers. 147/147 agree. This layer is deliberately modest — chosen executions, not semantic equivalence, never called a proof — and it is what keeps the theorems honest about which X they are theorems about.

the theorems

28/28 families · Weth10*.lean

Where the corpus samples, the theorems quantify. Public compiled-effect families cover all 28 runtime entries — reads, state transitions, the three typed callbacks, permit, flash loans, exact rollback and error genres. Above them sit the load-bearing claims: holder-flow conservation in ℕ, dormant-holder protection, a deployment root derived through the real block pipeline, and constructed withdraw/withdrawTo success at message and transaction altitude — the future-redeemability guarantee of § 5. Every statement ranges over the states, arguments, callbacks, and valid chain histories its quantifiers name, and every one is about the exact compiled bytes.

the boundary

assurance boundary · registries

The edge is published with the same care as the center. The README’s assurance boundary keeps three registers — formally proved, executably tested, not established — and the third is load-bearing: no deployed-runtime verification, no semantic-equivalence claim, no malformed-calldata closure, no key custody or inclusion, no gas, storage, or codehash parity. Deviations from the reference are governed, not forbidden: each is a registry row with a stance and evidence — WETH10’s registry currently holds zero accepted rows in its stated scope — and an observable difference, once discovered, must be restored or recorded. The registry is non-exhaustive; leaving a known divergence unrecorded is the one prohibited move.

the scope of the burden

No specification list is ever finished, and the port does not pretend otherwise. It answers, item by item, for everything it wrote — every proved specification and every differential expectation is offered as a statement of what the contract is for, individually contestable — and for anything it is shown, under the registry’s discovered-difference rule. It does not pre-accept burden for specifications no one has written. An earlier, more ambitious instrument that did — a standing wager over every feature-level truth of the deployed original — was retired in August 2026 as unadjudicable in principle; PORTING.md’s policy note records why.

claims end where evidence ends

A property believed but not yet proved is recorded as a counted verification debt, never asserted — asserting unproved properties is what every unverified contract already offers. When a property resists proof, the rule is: claim less, never assert more. The standing terms — the feature test, the interface/accident boundary, the publish-when-discovered rule that stops a stance being invented after a challenge — are PORTING.md’s. This page summarises it; that document governs.

WETH_DEVIATIONS.md — 5 rows, 2 now agreements FMINT_DEVIATIONS.md — vs. OpenZeppelin WETH10_DEVIATIONS.md — zero accepted deviations LIDO_CIRCUIT_BREAKER_DEVIATIONS.md — zero accepted deviations BEACON_DEPOSIT_DEVIATIONS.md — 5 rows, none behavioral LIDO_TRIGGERABLE_WITHDRAWALS_GATEWAY_DEVIATIONS.md — 3 accepted, 2 repaired OSSIFIABLE_PROXY_DEVIATIONS.md — 1 accepted deviation PRORATA_WETH_VAULT_DEVIATIONS.md — 9 rows, all pre-registered WETH10_COMPATIBILITY.md — the frozen boundary, one of four

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.

§ 10 Position

The penultimate form.

“…the assembly + Lean paradigm is the final form of software development.”

— Yoichi Hirai, The Final Form of Software Development (2026) — AI agents writing machine-level code, proved correct in Lean; cited in Vitalik Buterin’s A shallow dive into formal verification

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

the agreement

High-level languages exist to protect humans from machine-level detail, at the price of compilers, runtimes, and semantic distance between source and chain. If proofs — not familiarity — carry the assurance, and agents — not humans — carry the tedium, most of that protection is overhead. Hirai’s conclusion follows: write the machine’s own code, prove it in Lean, let agents do both. Everything on this page is downstream of taking that seriously.

the amendment

Modern agents are extraordinary; they are not all-powerful, and neither are the humans auditing what they produce. A tiny amount of structure over raw bytecode — Blanc’s is four constructors, at the cost of computed jumps — is disproportionately cheap leverage: control flow becomes a tree proofs can walk, the compiler becomes a theorem proved once and inherited by every contract, and a reusable proof ladder becomes possible at all. Keep the canvas blank; rule four faint lines on it.

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.

§ 11 The field

The lay of the land.

Blanc is one answer in a field of serious ones, and the honest way to be compared is to publish the comparison. Two families do most of the work. One writes verification-friendly code and proves things about what it wrote — the claims run deepest, and the price is leaving your existing source behind. The other verifies code that already exists — it meets you where you are, and pays for that reach in what it can state. Neither family dominates: which one you need mostly follows from whether your bytecode is already on chain.

read this first

This table is one project’s best effort to understand its neighbours, compiled from their public repositories, papers, and documentation as read on 2026-08-15. It is not an official survey; the author is not an expert in the systems featured; none of it was contributed to or proofread by their authors, and it may lag their repositories. If you maintain one of these projects and a cell short-changes you, file an issue — it will be treated as a defect, exactly like an overclaim about Blanc itself.

project	foundation	what it verifies	gas	liveness	where it stops
writes its own bytecode — verification-first languages & compilers
Blanc this project, over Jaune	Lean 4; Jaune’s executable EVM semantics at a pinned commit	its own four-constructor source, tied to the exact compiled bytes by a proved compiler; properties lifted to block and chain altitude	exact — proved equations, gas-exact in both run directions	constructed successful executions, at message and transaction altitude	cannot verify contracts already deployed; a new, deliberately bare language — § 8 is the bill
Verity LFG Labs	Lean 4 EDSL, compiled by way of Yul	contract properties of the EDSL program; reports a zero-axiom Lean layer; active, with strong documentation and a paper	not modeled, per its own trust documentation	—	Yul→bytecode goes through a pinned solc that is trusted, not verified
Clear Nethermind	Lean 4, over the EVMYulLean model	Yul programs, against a formal Yul semantics	—	—	claims live at the Yul level, not the deployed bytes; documents its Yul-model limitations
DeepSEA	Coq	programs in its own layered language, compiled toward EVM in the verified-compiler tradition	—	—	a research system
verifies bytecode that already exists
KEVM / Kontrol Runtime Verification	K framework; reachability logic over a full EVM semantics	arbitrary EVM bytecode, symbolically; Foundry-shaped entry through Kontrol; the mature incumbent, commercially supported	modeled in the semantics	all-path reachability is partial correctness — claims range over terminating paths	scaling proofs on large contracts remains expert work
Certora Prover	SMT, driven by the CVL specification language	arbitrary contracts at bytecode level, highly automated; the audit-market standard, with a long production record	not modeled	—	commercial and closed; soundness is modulo its documented approximations — loop unrolling, summarization
hevm	symbolic execution	EVM bytecode — symbolic tests and equivalence checking between two bytecodes; the long-standing open engine of this family	—	—	an engine more than a full stack; bounded-exploration caveats apply
Halmos a16z	symbolic execution over Foundry test suites	your existing tests, with symbolic inputs — specifications are tests, which is also its adoption path	—	—	bounded; a property is checked as far as the tests and unrolling reach, not proved in general
EquiVM Argot Collective	Lean 4, over a ported EVM model	deployed bytecode, by refinement against specifications in a Solidity-like spec language; WETH9 and a MakerDAO suite completed, more scaffolded	out of scope on its published roadmap	its own sources note termination is not forced — an out-of-gas case can discharge the equivalence obligation	per-contract selector hashes enter as axioms; reasoning about what solc emits is re-earned per compiler version
Verifereum	HOL4; its own executable EVM semantics, with near-complete execution-spec-test coverage	aims at deployed contracts, through program-logic and compiler work over that semantics; the closest ITP semantic peer	modeled — its semantics passes the ecosystem’s corpus	—	contract-verification tooling younger than the K ecosystem’s

Table 1 — the lay of the land, as read from public sources on 2026-08-15. A “—” cell means we found no documented claim, which may be a fact about our reading rather than about the project; “where it stops” records each project’s own published boundary where one exists. The Blanc row is held to the same register as this whole page; every other row is held to the disclaimer above.

the layer under the table

Every stack above stands on an EVM semantics, and those are a landscape of their own: EELS, Ethereum’s canonical executable specification — the oracle inside Blanc’s own differential gates — alongside Jaune (Lean 4), Verifereum’s HOL4 semantics, KEVM’s K semantics, and Nethermind’s EVMYulLean. A different project family — evm-asm, evm-sail — verifies implementations of the EVM itself: “is the machine right”, where everything in the table asks “is the contract right”.

deliberately off the table

solc’s built-in SMTChecker and the property fuzzers — Foundry’s, Echidna, Medusa — are valuable, cheap, and not in the business of machine-checked functional specification; they complement the table rather than competing with it. Early-stage entrants (powdr’s Yul compiler work, small verified-WETH exercises) are noted here rather than rowed. And from outside the EVM: the one ecosystem where revert-freedom is checked routinely, by default, at framework scale is the Move Prover’s aborts_if discipline — a different VM, and a standing reminder of how much ground this field, Blanc included, has left to cover.

the ceiling, and where it was already cleared

Impose three asks at once — verify the deployed bytecode, so no compiler is trusted; emit a proof someone else can check, so no solver is trusted; and state a real contract property, not a semantics and not a refinement — and the EVM literature thins out fast. Read on 2026-08-19, nothing else on this table cleared all three much past a wrapper’s solvency; Blanc’s own furthest point on those terms is now the deposit-contract port of § 6 — a different artifact from the one Runtime Verification verified, and no claim about that one. The near misses deserve naming precisely, because they are near: Runtime Verification’s eth2 deposit contract and MakerDAO vat proofs are genuinely bytecode-level and reach well past any wrapper, and Certora’s production record reaches further still. All of them drop the second ask and leave no artifact a third party can re-check. The complexity is available; the checkable proof of it is not.

Off the EVM it has already been done, and above a wrapper. Nomadic Labs verified Tezos’ Liquidity Baking CPMM in Coq by way of Mi-Cho-Coq — at the level of the contract’s Michelson, with a kernel-checkable proof, establishing that the market-maker invariant is strictly increasing and that all three contract balances stay strictly positive, for a contract live on mainnet at protocol level. That is a solvency-class property on an automated market maker, and it clears every ask above. The reason it was reachable there is structural: on Tezos the deployed artifact is Michelson — typed, structured control flow, no computed jump targets — so the distance between the code on chain and the vocabulary a property is written in is short by construction. On the EVM that distance is the entire problem, and every project in the table above is a different way of paying it. Blanc’s answer is to refuse to emit code that opens the gap rather than to close it after the fact — which makes the Tezos result an existence proof that this family works once the gap is shut, and somebody else’s result rather than evidence for this one. Both stacks still trust their own semantics, Mi-Cho-Coq’s Michelson model and Jaune’s EVM model alike: the assumption neither ask removes, only relocates.

How to read it for a decision: if your bytecode is already deployed and cannot change, the second family is your only option, and it is a good one. If you can still choose the source, the first family trades familiarity for depth — Verity keeps more of the familiar toolchain and trusts solc at the boundary; Blanc spends the familiarity and buys the exact bytes, exact gas, chain altitude, and constructed liveness. § 8 prices that trade honestly. This table will be re-read and corrected as the field moves; it is a map, not a defense.

§ 12 Who this is for

Three ways in.

Teams with an invariant worth a proof

You maintain a wrapper, a vault, a bridge component — something whose entire job is a property you can say in one sentence. Blanc’s worked examples are exactly that shape. Bring the sentence; the ladder from “compiled bytes” to “every reachable chain state” is already built — § 6 shows it climbed, ten contracts over.

start: WETH10_COMPATIBILITY.md — a behavior, frozen
then: Blanc/Weth10FutureRedeemable.lean — the redeemability guarantee, end to end

Proof engineers & PL researchers

A live laboratory for proof-cost economics: which abstractions let the fourth contract cost less than the third, where callback-crossing machinery generalises, what a dispatcher-combinator layer owes its clients. ~490,000 lines of worked answers, with the open questions in the goal ledgers.

start: Blanc/Semantics.lean — the four constructors
then: Blanc/Ladder.lean · Blanc/Forward.lean — the reusable spine

Auditors & professional skeptics

This project keeps a register you can attack: deviation rows with stances, counted verification debts, and falsifier tables. Every proved specification and differential expectation is offered as a statement of what the contract is for — contest any item and an answer is owed. And if you find a divergence with no row, that is a defect by the project’s own rules — file it.

start: WETH10_DEVIATIONS.md — zero accepted deviations
then: scripts/GATES.md — every gate, scale, and pass criterion

§ 13 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.

Check the proofs

no fixtures required — this side is proof, not testing

$ git clone https://github.com/skbaek/blanc $ cd blanc && lake exe cache get && lake build $ scripts/check.sh --no-build $ scripts/check-claims.sh

check.sh walks every constant of the library once for axioms, and finds the 2247 leaf results — failing on any axiom beyond the three, on sorryAx, and on any native_decide-style escape. check-claims.sh then Lean-checks the exact statements of the protected WETH10 redeemability set, the Lido Registry mutation, enumeration, local-observability, exact constructor/message/transaction/block, direct-root, and rooted-future boundaries, the proxy-pair upgrade boundary, and the PRORATA, ERC-4626 vault, BeaconDeposit, and DRIP headline sets, so a weakened conclusion fails as loudly as a broken proof. Both projects open with lake exe cache get; skipping it means compiling mathlib from source — hours instead of minutes.

Read it in order

the shortest honest path through the claims

the behavior: WETH10_COMPATIBILITY.md — “right”, written down: the frozen boundary, row by row
the rules: PORTING.md — what a port claims, the deviation discipline, and the note retiring the old wager
the map: README.md — every module, every theorem family, the assurance boundary
the gates: scripts/GATES.md — each gate’s command, scale, runtime, and pass criterion
the showcase: Blanc/Weth10FutureRedeemable.lean — read the statement, then its docstring’s scope notes
the claim map: LIDO_CIRCUIT_BREAKER_ASSURANCE.md — every CircuitBreaker claim, mapped to the theorem that carries it, non-claims included
the second map: BEACON_DEPOSIT_ASSURANCE.md — every deposit-contract claim, with its differential channel or an honest “none”
the third map: docs/PRORATA_WETH_VAULT_CLAIM_MAP.md — every vault sentence: carried by a theorem, by finite evidence only, or not carried
the semantics: Jaune — the machine under all of it, with its own evidence page

“Every freedom” is claimed precisely: each claim in § 1–6 is backed the way its own section states — theorems with pinned axiom closures where it says proved, dated gate output where it says measured. It does not mean every true property of every contract has been proved — § 9’s claim-discipline governs, and declared non-claims are listed in each contract’s registry.
Blanc was previously presented as Jaune’s case study; it is now a sibling project with its own charter. Jaune remains the semantics every Blanc theorem is stated over, pinned by immutable commit — see the Jaune page for its conformance evidence.
Every figure about this repository on this page is drawn from a committed report, registry, gate summary, or theorem in the repository; the snapshot was re-derived from the committed tree on 2026-09-25. § 11’s landscape table is the one deliberate exception — it describes other people’s projects, on the terms its own disclaimer states. Each gate line says which run it comes from: the WETH10 differential and fixture lines are verbatim output of the exact-candidate 2026-09-03 UTC run, the layering line of a 2026-09-25 run, and the axiom-audit and claim lines render their gates’ verdict wording at counts a static gate derives from the committed audit and pin files. One long line is wrapped and ellipses mark elision; the differential line continues “… 7 state-mutating reentrancy rows, 26 STATICCALL-context rows, 69 oracle calls traced, 8 channel falsifiers live.”
Spelled out, because the boundary rewards precision: when a Blanc contract reimplements WETH9 or WETH10, the deployed original is the reference, never the subject — nothing on this page proves anything about the contract at the reference address. And byte-identity is a non-goal permanently, not merely so far: a compiler that chases another compiler’s bytes inherits its dispatcher, its stack discipline, and its bugs, and can justify nothing beyond “same as before.” The standing statement of what a port claims and never claims is PORTING.md.

Keep every freedom.Except one.