What a conservation guard cannot see: five findings that passed a correct, enforced, tested invariant

The useful artefact in this article is not a theory. It is a ratio. A conservation guard that was correctly written, enforced at thirteen entry points including both administrative funding paths, exempt for nobody, and covered by a dedicated test, was nonetheless silent for six of the seven vulnerabilities subsequently disclosed against the staking contract it protected. The seventh moved the residual quantity the guard does observe, and surfaced against a different check.

That partition is publicly verifiable — the findings have identifiers, external reporters and commits — and it is a concrete instance of a claim usually argued in the abstract: that single-trace verification, done properly and taken seriously, can still leave the majority of a real system's defects structurally out of reach. Nothing below is offered as evidence that invariant-driven design fails. It is one honest measurement of what one good invariant could not see.

The guard, and why it is a good one

The check compares, across every value-moving transaction, the change in what the contract actually holds against the change in what it claims to owe, and reverts if those two deltas diverge by more than a dust tolerance. Both sides are recomputed from state rather than read from calldata, so there is no attested quantity anywhere in it. It is applied structurally at every entry point that can move value, administrators included. Violation reverts.

It is also deliberately differential rather than absolute, and that choice is better engineering than the stronger-looking alternative. An absolute form — holdings must always cover obligations — would have turned a few wei of rounding drift into a permanent denial of service for every user. The differential form fails only the transaction that actually leaks. An invariant costs the liveness it forecloses, and the stronger predicate here would have been a denial of service dressed as rigour.

Dimension and silence

An invariant is usually discussed as a predicate. That framing hides half of it. An invariant is two objects: a map from system state onto some observable value, and a relation that must hold over that value. Conventional practice argues about the relation. The map is where the design decision actually sits. In the formal-methods literature the map is an abstraction function, the states it cannot separate are its concretisation, and what it discards is precision loss; none of that vocabulary is ours, and using the established names is what makes the measurement checkable rather than folkloric.

Call the set of state changes the observable cannot distinguish its silence. The one statement that does the work is a contrapositive and therefore trivial — and trivial in the way a change of variables is trivial. If the guard is enforced everywhere it could be violated, then any harmful transition that the guard did not fire on lies inside the silence. Its content is procedural: the surviving attack is never outside the silence, so search there. An audit that re-examines the guard is looking in the one place the attack provably is not.

invariant  =  I : S -> V        (the observable — the dimension)
           +  R subset of V x V (the relation — the predicate)

Sil(I,R)   =  { transitions the code admits that R accepts }

H(s, t(s)) AND the guard never fired   =>   t is in Sil(I,R)

Where this guard's silence comes from

The guard reads only one combination of its two components, so its effective dimension is a single scalar: the residual between holdings and obligations, bounded per transaction. The state it ranges over contains one record per position — principal, debt, boost multiplier, lock end, index snapshots — plus the emission clock. The guard compresses that entire space onto a line, and there are five independent families of change that move along the line by zero.

The first is the fibre of a sum. Obligations are computed from totals, so for any aggregate distributed over positions, every reallocation of that aggregate is invisible. With a thousand positions the guard observes one direction and is blind along nine hundred and ninety-nine. The second is temporal attribution: when value was earned, who was present while it accrued, and which interval is being priced appear nowhere in the observable. The third is the fibre of a delta — common-mode change and all accumulated historical drift, deliberately, since the absolute form would brick the contract. The fourth is the dust tolerance, which is per transaction and therefore composes: N transactions carry N times the tolerance even though each is individually inside it. The fifth is created by the arithmetic rather than by the statement: a saturating subtraction inside the obligations computation collapses an entire inverted region onto zero.

Silence is created by arithmetic, not only by omission, and that is the part engineers routinely miss. A sum is blind to how it was split. A difference is blind to common-mode change. A tolerance is blind below the tolerance, and blind to N of itself over N transactions. A saturating subtraction collapses a whole region of state onto one value, and the region it collapses is usually the pathological one. Adding a second guard narrows nothing unless its own silence is different — coverage is set intersection, not a count.

The five findings, and why they are the same finding

Five of the seven disclosed staking findings are one error wearing different clothes, and recognising that is more useful than any individual description. Each computes a quantity that accrues continuously — interest, emission weight, a stake's share — by sampling it at the moment someone happens to interact, and then applying that sample to the whole elapsed interval. In the language of integration, they evaluate a path integral by taking the value at the right endpoint and multiplying by the width of the interval.

When nothing changed during the interval, that is exact, which is why it survives review. When the rate moved, it silently attributes the final rate to the entire period, and the difference is taken from one participant and given to another. With a rate that rises linearly from 0.4 to 1.0 across an interval, the true accrual is 0.70 and the amount charged is 1.00 — an over-attribution of more than forty per cent, produced by arithmetic that looks correct on every single line.

Each non-constant factor sampled at the right endpoint generates one member of the family. Sampling the rate at the endpoint produces retroactive repricing of an elapsed interval. Sampling the total weight at the endpoint produces just-in-time capture, where a participant absent for the whole window takes a share of it by being present at the instant of realisation. A stale stored multiplier produces an unearned boost applied to newly added principal. All of them are redistributions: the residual the guard observes does not move, by construction, so the guard is delta-neutral on both sides and never fires.

V_i(t0 -> t1)  =  INTEGRAL_{t0}^{t1}  rate(s) * w_i(s)/W(s)  ds        (owed)

lazy form      ~=  rate(t1) * (t1 - t0) * w_i(t1)/W(t1)                  (charged)

exact only if every factor is constant across the interval.
rate(t1) sampled  -> retroactive repricing
W(t1)    sampled  -> just-in-time capture
stale w_i         -> unearned multiplier

The sharpest available statement: these are 2-safety properties

The reason no better predicate over the same observable would have caught them is not that the guard was weak. It is that the properties violated are not single-execution properties at all. "The interest charged to a position does not depend on which transaction drove the sweep" is a relation between two executions. So is "two positions identical in principal, debt and unlock time receive an identical multiplier". So is time-additivity. In the Clarkson and Schneider classification these are 2-safety properties, and a 2-safety property is not expressible as a predicate over any single execution, at any level of effort.

So the guard did not fail. It could not have succeeded. That is a structural impossibility result available off the shelf, and it upgrades the observation from a war story into a categorical statement — at the cost of a citation and of not claiming it as ours. The theory is not ours: abstraction and its precision loss, the hyperproperty classification, vacuous satisfaction, metamorphic relations, coverage by mutation. All of it is established work with established names. The measurement is the contribution.

The control case, and the boundary of the claim

The sixth finding inside the silence and the seventh outside it form the honest edges. One member of a second, smaller family advances a clock without writing its dual: an emission window closes with nobody eligible and the value is stranded, owed to no one — the purest instance of the sum fibre, since the aggregate is merely recategorised. The other member of that family is the control case: an underwater exit that removes a debt without recording the bad debt it leaves behind. That one is not a redistribution. It changes the relation between what is held and what is claimed, and it surfaced on the absolute solvency axis, which is a different dimension enforced by a different check. The partition falls exactly where the method says it must.

One boundary must be stated rather than glossed. That the control case lies outside the redistribution class is recorded in the findings register. Whether the differential guard would additionally have fired in the offending frame has not been verified against a re-execution, so the claim we publish is the one that is checked: the control case is visible on the absolute axis, and the other six are not visible on either.

And the epistemic point, which is the reason any of this matters. For the entire period those defects were live, the guard was green — not weakly green, but structurally enforced, tested and honest. A correct invariant over the wrong observable produces false confidence, and false confidence is worse than no invariant, because it stops the search.

What replaces it, and what that costs

The answer is not a stronger conservation law, because by the classification above there cannot be one. The observable that would have seen these is per-principal attribution, and enforcing it takes two mechanisms, neither of which is a second modifier. At test time, metamorphic relations supply the oracle: driver-invariance (the cost charged to a position may not depend on which transaction drove the sweep), time-additivity (accrual over a whole interval equals the sum over any partition of it), history-independence of price, and continuity of any throttle that would otherwise be a cliff. Each is a relation between two executions and needs no hard-coded expected value.

On-chain, the discharge is structural: advance the accumulator before any write that changes its inputs, which forces the integrand constant across each settled interval and makes the right-endpoint rectangle coincide with the path integral. That costs nothing per position and is satisfied by construction rather than by a runtime check — and that is exactly why its epistemic status is lower than the guard's. It will not revert if a future edit breaks it. The honest closing sentence is not "we closed the dimension"; it is "we named the dimension, discharged it structurally, and pinned it with two-execution tests".

The practice we would ask a reader to take away is smaller and cheaper than any of it: write the guard as an expression over named state, then write the list of things that can change while that expression does not, and publish the second list beside the guarantee. That deliverable has a fixed shape — this guarantees X; it permits Y and Z — and almost nobody writes the second clause.

Related engineering

• The decomposition law: why one contract is a monolith and the other is not ›
• Invariant-driven design: what a conservation law proves, and the dimension it cannot see ›
• When invariants meet time: the vulnerability class conservation cannot detect ›