Invariant-driven design: what a conservation law proves, and the dimension it cannot see

An invariant is a property a system promises will hold no matter what any actor does: a statement of truth the code itself refuses to violate. In a smart contract it is enforced structurally — the transaction that would break it reverts, so the forbidden state is not merely observable, it is unreachable. This is a stronger guarantee than a test, which only shows the property held for the inputs someone thought to try. An invariant is the discipline of compute, do not trust, made mechanical: the system does not ask you to believe it is solvent, it makes insolvency a state it cannot enter.

The engineering question is not whether invariants are powerful — they are the strongest tool available on-chain — but what a given invariant actually promises, and, more importantly, what it is silent about. That silence is where the next defect lives.

Two families of tool, one hard requirement

The verification landscape splits cleanly. Property-based fuzzers — the invariant runners in Foundry, Echidna, Medusa — drive a contract through long random sequences of calls and check the property after each one. They are extraordinary at finding counterexamples, and most deployment-stage bugs are caught this way. But a fuzzer that never finds a violation has proven nothing: absence of a found counterexample is not a proof of absence. Its strength is falsification, not correctness.

The second family — symbolic checkers and formal provers such as Halmos and Certora — reasons over the entire range of valid inputs at once. When a property passes there, it holds for all inputs, not just the sampled ones; when it fails, the tool hands back the exact witness. This is proof rather than evidence, but it is bounded by state-space and specification limits, and it is expensive.

Both families share one requirement that no tool removes: a human must write the invariant. The machine checks the property you gave it, flawlessly, and says nothing about the property you did not. Every published catalogue of these tools ends on the same sentence — they still require someone to state the right invariant first. That sentence is the whole subject of this article.

The ephemeral case, where invariants are nearly complete

Consider a system that opens and closes inside a single transaction: an exact-input swap. It pulls an input, executes, pays an output, and returns to rest holding nothing. The state carries no history between calls; a defect has a window measured in one block and a blast radius that is local to that trade. For a system shaped like this, a small set of invariants is very close to complete.

The core one is per-transaction value conservation: snapshot the real balance and what the protocol owes before the body runs, and after it require that the change in the balance equals the change in what is owed, within a dust tolerance. Any transaction that itself leaks value fails; accumulated historical drift cancels out, so a legitimate action is never reverted for a books-are-a-few-wei-off reason. Pair it with a minimum-output floor that is re-derived on-chain from the real trade rather than read from caller-supplied data, and the manipulable surface shrinks to almost nothing.

What an invariant actually guarantees

Here is the load-bearing observation. An invariant guarantees exactly the dimension it measures, and nothing adjacent to it. A conservation invariant is a statement about QUANTITY: it answers how much value exists, and it answers it perfectly. It is completely silent about every other property the system might need to be true — who is owed that value, when it was earned, whether an authority can redirect it, whether an honest user can still exit.

This is not a weakness in a specific invariant; it is the nature of the tool. A correct invariant over the wrong axis passes on every block, forever, while the real defect compounds underneath it — and because the guard is green, nobody looks. A correct invariant that covers the wrong dimension gives false confidence, and false confidence is worse than none, because it stops you searching.

Why "the tests pass" is evidence, not proof

Coverage is not correctness. A suite that passes tells you the properties you wrote hold under the sequences you explored. It is genuine evidence and it should be demanded. But it is bounded twice over: by the inputs the fuzzer reached, and — the deeper bound — by the imagination of whoever chose the invariants. The bug that survives is almost never in the property you stated and tested; it is in the dimension you did not think to name, so no property was ever written to guard it.

For a system that lives in the instant, the set of dimensions is small enough that a disciplined team can enumerate it. The moment a system starts to carry state across time, that enumeration stops being complete — and a whole family of defects appears that a conservation law, however perfectly enforced, is structurally unable to detect. That is the subject of the companion piece.

Related engineering

• When invariants meet time: the vulnerability class conservation cannot detect ›
• Invariant-driven design: how a codebase can make an AI stop guessing ›
• Provable staking solvency: an invariant anyone can check, any block ›