Blanc/implementations/ports
CircuitBreaker.
The port of the CircuitBreaker that Lido deployed at 0x6019…B2F7 — an emergency brake in which an admin grants pauser addresses time-limited authority over registered protocol contracts, and a pause spends the authorization before the target ever gains control. In April 2026 an industrial verification campaign on the same Registry source closed 38 of 41 properties and reported three coupled preservation obligations unresolved. Blanc’s port proves one combined Registry invariant, designed together with the representation, from which all three obligation shapes fall out as corollaries — then roots it in a proved official-parameters deployment and carries it to every reachable future.
A port never claims byte identity — PORTING.md governs what is claimed and what never is. What makes this port distinctive is the assurance register: 75 rows mapping every quotable claim onto the exact declarations that carry it, the premises they require, the axioms they depend on, the gate that owns them — and, in every row without exception, what the row does not claim.
Fig. 1 — two CircuitBreaker gates, verbatim, ellipses marking elision (differential: exact-candidate run 2026-09-03 UTC; register verifier: run 2026-09-25 UTC): the differential matrix beside the locked Solidity reference, and the register verifier that fails if any cited declaration, axiom set, or non-claim phrase drifts from the tree it describes. The differential line continues “… 82 Solidity CALL/STATICCALL traces; 15 positive artifact checks + 1 runtime corruption; 16 live channel/projection/identity/manifest falsifiers.”
What the port proves
One invariant, carried to every reachable future.
In April 2026 an industrial verification campaign on the same Registry source closed 38 of 41 specified properties and reported three coupled registerPauser preservation obligations unresolved — membership equivalence, clean state after removal, global count conservation — naming circular inductive dependencies, four mutation modes, and swap-and-pop as the difficulty. Blanc’s answer is structural: one combined Registry invariant, designed together with the storage representation, from which all three obligation shapes fall out as corollaries — then rooted in a proved official-parameters deployment through the full Prague block pipeline, and carried to every reachable future with no premise about anyone else on the chain.
From a checkpoint whose state holds the exact compiled runtime with coherent Registry storage, every state reachable along a configured valid chain is still stable — whole blocks, every transaction anyone sent, arbitrary contracts doing arbitrary things.
theorem chainUsing_preserves_registryStable (dp : DeployParams) (ca : Adr) (cfg : ChainConfig) (checkpoint future : BlockChain) (reach : BlockChain.ReachUsing cfg checkpoint future) (stable : RegistryStable dp ca checkpoint.state) (hcov : ∀ t f, cfg.forkAt t = .ok f → CoveredFork f) : RegistryStable dp ca future.state
Read what is absent — no premise about the bytecode at any other address, no non-reentrancy condition, no direct-call-only restriction, no honesty asked of the contracts it pauses, no noninterference assumption, and no identification of the post-callback entry list with the checkpoint’s. What is present is one schedule premise: every fork the configuration selects is one the proofs cover — Prague, Osaka, BPO1, or BPO2 — which Jaune’s mainnet schedule satisfies and an Amsterdam-scheduled chain does not. The owning gate probes all 104 public theorems of the family for exactly Lean’s three standard axioms and admits no exception table. And the checkpoint hypothesis is not a supposition: DeploymentRoot discharges it for the one official deployment shape, and its projections carry exact code, a coherent witness, and global count conservation to every reachable boundary.
RegistryWitness -- one ordered entry list witnesses every projected Registry region; raw slot equality and global Keccak-injectivity intentionally absent membershipEquivalence_registerPauser -- assignment ≠ 0 ⇔ index ≠ 0 ⇔ array occurrence, position unique — no execution premise cleanStateAfterRemoval_registerPauser -- swap-and-pop: both lookup slots zeroed, dead tail cleared, moved element's index repaired globalCountConservation_registerPauser -- Σ per-pauser counts = registry length canonicalDeploymentStep_ establishes_root -- the official input through message, tx, and Prague block → DeploymentRoot, empty witness chainUsing_preserves_registryStable -- the theorem above
At the moment an arbitrary target first receives control, its own assignment cell is already zero and the reentrancy lock is held, with nothing written between pauseAfterSet entry and the CALL — and no hypothesis constrains the target’s code. Re-entering pause from that mid-call state takes the refusal arm: it reverts with the reentrancy payload and writes nothing.
The liveness boundary is exactly timestamp < expiry: a zero-count caller errors SenderNotPauser before any liveness test, an expired caller errors after it, and neither moves storage. A heartbeat extension whose sum would wrap reverts with a source-exact Panic(0x11), restoring owner state.
Exactly three premises — the pre-execution base, the strict official block envelope, and one actual successful configured Prague-only transition — and from them the proof reconstructs the creation message, receipt success, the exact installed runtime, the frozen official constructor arguments, and an empty Registry witness. One deployment shape only: no clone, factory, proxy, or CREATE2 path, and no claim about the mainnet transaction it mirrors.
So Blanc succeeded where an industrial prover failed?
pushbackNo — and the register forbids that sentence. What may be said: a named campaign left three coupled Registry preservation obligations open, on Registry source blob-identical across the mitigation, deployment-source, and v1.0.0 revisions; Blanc closed those obligation shapes for its own faithful port, by making all three corollaries of one invariant designed together with the representation. A tool given a different problem — recovering properties from an existing artifact rather than designing property and representation together — is not a tool that failed. And one link in the comparison is a named gap, not a verified fact: the cross-revision source-blob identity is taken from the cited report, and no gate here witnesses it. A reader who needs it verified must check the reference’s Git history directly.
“Every reachable future” — including an admin interfering mid-callback?
pushbackYes, by claiming exactly the right thing. The history witness is existential, not the same list: an admin legitimately re-entering during a callback may register a pauser, so the guarantee is that some coherent entry list describes the storage — never that the checkpoint’s list survives. Mid-call, after unregistration and before the callback returns, an unregistered address still reports live — real source behaviour, pinned in the differential matrix, and the reason no callback-time count/expiry coherence is claimed anywhere in the register. The one place an exact final state of one successful pause is claimed rests on PauseSuccessNoninterference, a premise whose own docstring opens “Assumed, not derived” — and two differential rows measure that arbitrary callee code can falsify either of its equalities, so the assumption is demonstrably non-idle. The history family carries no such premise, and the register forbids generalising the assumption into one that does.
Does any of this say Lido’s protocol is safer?
pushbackThe claims stop where the evidence stops. Two configured direct-installation worlds now construct successful public pauses through the separately verified TriggerableWithdrawalsGateway, for the ordinary and infinite-sentinel durations. In those exact worlds the target’s canonical true is joined to the real gateway executions and paused storage; outside them it remains evidence only that an arbitrary target reported success. This is no universal liveness or all-world gas claim, and it says neither that an external actor will submit a transaction nor that a current deployed target has this state. Nothing verifies the Solidity deployed at 0x6019…B2F7: its address, transaction, and block are provenance identifiers only.
The 75-row assurance register maps every quotable claim above onto the exact declarations that carry it, the premises they require, the axioms they depend on — and, in every row without exception, what the row does not claim. Its fourteen load-bearing non-claim phrases are pinned by the gate that verifies it, so a sentence that outruns its theorem fails CI rather than surviving as prose.
How we know it is the CircuitBreaker
A claim map, and evidence that answers to it.
“Right” was written down before it was argued: LIDO_CIRCUIT_BREAKER_COMPATIBILITY.md freezes the reference’s public conformance boundary endpoint by endpoint, and the assurance register maps every claim onto its evidence — with the axiom column checked transitively against Lean and every load-bearing non-claim pinned, so a quoted sentence that outruns its theorem fails a gate rather than surviving as prose. Two layers discharge the claims — open the one you want to audit.
▸Differential evidence — the sanity layer175 rows vs the locked Solidity v1.0.0 · six channels · 464 resource boundaries
check-lido-circuit-breaker-differential.sh executes the exact compiler-derived Blanc artifact beside the independently locked Solidity v1.0.0 reference in a pinned EELS Prague interpreter — 175 rows, agreeing on all six credited channels: status, exact returndata, logical projected state, ETH, ordered logs, and retained call traces. The rows are not gentle: constructor errors and precedence, Registry mutation histories seeded by 144 causal transactions, time and overflow edges, nested same-target and different-target reentry, callback interference, and 82 live CALL/STATICCALL traces retained across rollback — including the mid-call coordinate where an unregistered address still reports live, pinned as real source behaviour rather than papered over.
A separate gate executes what the deployment theorem then quantifies: check-lido-circuit-breaker-deployment.sh carries one strict singleton type-2 Prague creation block through pinned EELS, with 18 positive assertions and 26 live finite mutants — feasibility and cross-evaluator evidence only, never a Lean premise.
The register stays modest on purpose: finite rows on chosen inputs, message calls rather than blocks — the campaign builds no block and no receipt — and none of it is ever called a proof. This layer’s job is to keep the theorems honest about which contract they are theorems about.
▸Proven functional specifications — the quantified layerendpoint families · write authority · compile witness
Where the matrix samples, the theorems quantify — over storages, entry lists, callees, and valid chain histories, always about the exact compiled bytes: lidoCircuitBreakerCode_compile exposes the exact-bytes equation for arbitrary deployment parameters, and every statement below hypothesises those bytes in so many words.
registration · pause · heartbeat -- typed endpoint families over the production dispatch list: guards, effects, exact rollback runtimeWriteAuthority_of_rawFrameRoot -- every raw SSTORE in an exactly-invoking frame classified to one of 20 frozen source sites, with role, guard, and entry fact — and no success, commit, or settlement premise
These families stop where conformance stops: they say the artifact dispatches, guards, writes, calls out, and rolls back exactly as the frozen boundary says it must. The Registry invariant, deployment root, and open-contract history family that stand on them are stated in full in the results section at the top of this page. The port’s 290 audited theorems sit in the repository-wide axiom audit, and check-claims.sh pins the exact statements of the protected Registry-mutation, enumeration, observability, and deployment boundaries.
Deviations
Zero accepted — and what that does and doesn’t mean.
LIDO_CIRCUIT_BREAKER_DEVIATIONS.md accepts no behavioral deviations: zero accepted rows, zero pending, and no unknown-mismatch allowlist. Agreement on the finite matrix is recorded as evidence, not inflated into a proof that no mismatch exists, and the registry’s standing rule does the real work: a future mismatch in the frozen surface is a defect or a new explicit conformance decision — it may not be silently moved into an “accepted” section. Silence is the one prohibited move.
The registry distinguishes behavior from implementation. Blanc keeps its freedom in: runtime and initcode bytes, code hash, dispatcher shape, and instruction sequence — never citable as Solidity-byte equality; raw persistent and transient storage keys and layout, since the comparison projects both worlds to logical Registry, expiry, and pause state; exact gas and out-of-gas thresholds, under the declared adequate envelope; and private helper factoring — so long as declared status, returndata, projected state, ETH, ordered logs, and call traces remain compatible.
The explicit exclusions are load-bearing: no operational event delivery, reorg, or finality claim; no callback-time count/expiry coherence; no target truth for an arbitrary target, and no composition of the full public pause result except the gateway’s, for its two constructed worlds; no deployment shapes beyond the one official direct creation; and no verification of deployed Solidity. The normative target is locked by scripts/lido-circuit-breaker-reference.json — the vendored v1.0.0 source under content-addressed digests — so “compared against what, exactly” always has a one-line answer.
Deltas
Size, and gas — measured, and bounded honestly.
| quantity | value | status |
|---|---|---|
| runtime size | 4,282 B | compiler-derived, digest-pinned |
| deployed CircuitBreaker runtime | 4,584 B | locked reference — the oracle anchor |
| full CREATE input | 5,122 B | vs 5,638 for the reference |
| successful construction gas | 906,729 | vs 967,777, measured in pinned EELS |
| adequate resource boundaries | 462 / 464 | strictly cheaper; the 2 declared OOG controls equal, none dearer |
| completion thresholds | 33 / 33 | exact minimum-gas searches, none above Solidity’s |
The port does not claim universal gas dominance, and the registry says why in so many words: Blanc’s mandatory structured dispatch may carry a small intrinsic overhead relative to a direct-jump implementation, so a universal claim would be false rather than merely unproved. What is committed is the finite vector above — every boundary digest-pinned, with falsifiers that must keep failing — and exact gas parity with the deployed original is a declared freedom, not a goal.
Unlike the WETH10 page’s closed-form gas equations, these figures are measurements against the pinned oracle, and the page labels them as such rather than promoting them. The differential evidence is specifically under the pinned Prague EELS; a separate dated BPO2 lane replays only the pause and query shared with the gateway, and nothing here implies deployability or cost on any other fork.
Notes
What the build taught.
The exact final state of one successful pause rests on PauseSuccessNoninterference, a premise whose own docstring opens “Assumed, not derived”: the callee, handed control mid-pause, did not move the caller’s count or the heartbeat interval. Two differential rows — overflow-pause-post-callback-count-positive and overflow-pause-post-callback-interval-change — measure that arbitrary callee code can falsify either equality, so the assumption is demonstrably non-idle, cited in the theorem, the module header, and the register alike. The history family carries no such premise, and its gate’s pin discipline keeps it from ever acquiring one silently.
The three open obligations were reported hard for a reason — circular inductive dependencies, four mutation modes, swap-and-pop. Blanc’s move was not a stronger prover but an earlier decision: design the invariant and the storage representation together, so membership equivalence, clean removal, and global count conservation become corollaries of one RegistryWitness rather than three separately maintained facts. The lesson generalises: when a property is hard to recover from a representation, the leverage is in choosing the representation — and a port that owns its artifact gets to choose. What this does and does not claim about the campaign itself is stated beside the theorem, in the results section.
Boundary, restated: nothing on this page verifies the Solidity artifact deployed at 0x6019…B2F7 — its address, transaction, and block are provenance identifiers only. Two configured direct-installation worlds construct successful public pauses for the ordinary and infinite-sentinel durations, joining the real gateway executions to paused storage. They do not establish universal liveness, an all-world gas bound, external submission, or current deployed-chain state; outside those worlds a target’s canonical true still means only that it reported success. The full boundary — fourteen pinned non-claim phrases — lives in the assurance register, in the honest register.