Invariant testing: writing properties that find real bugs

Xora Labs Engineering  ·  11 min read

Unit tests check the cases you thought of. Invariants check the cases you did not, which is where the money goes.

The difference that matters

A unit test asserts that a specific input produces a specific output. It is a statement about one example. An invariant asserts that some property holds after any sequence of valid operations, whatever those operations were. It is a statement about the system.

That distinction is the whole value. Exploits are rarely found in the examples the developer wrote down. They live in orderings nobody considered: deposit, borrow, donate, a reorg, then withdraw.

What makes an invariant worth writing

A good invariant is a sentence you would be willing to put in a whitepaper. If it is true only under normal usage, it is a unit test wearing a costume.

• Solvency. The protocol's assets are always at least its liabilities. This one finds more real bugs than the rest combined.
• Conservation. The sum of balances equals total supply. Shares issued match assets accounted for.
• Monotonicity. An index that should only ever increase never decreases. A vault's price per share does not fall absent a realised loss.
• No free value. No sequence of operations lets an account end with more than it deposited plus its legitimate share of yield.
• Access. No unprivileged caller can reach a state only an admin should be able to reach.

Why campaigns fail to find anything

Most disappointing invariant runs fail for one of four reasons, and all four are fixable.

• The handler cannot reach interesting states. If the fuzzer can only deposit and withdraw, it will never construct the borrow-then-liquidate-mid-reorg sequence where the bug lives. The handler is the test.
• Inputs are bounded into safety. Clamping amounts to sensible ranges is necessary to avoid wasting runs on reverts, but clamp too tightly and you have excluded the edge you were looking for. Zero, one wei, and the maximum are where rounding bugs live.
• The invariant is too weak. "Total supply is non-negative" is trivially true for an unsigned integer. It tests nothing.
• Ghost variables are missing. Many real properties are about history rather than current state: total ever deposited, total ever withdrawn. Without tracking them in the handler, the property cannot be expressed.

Reading a failure properly

A failing sequence is not the bug. It is one path to the bug, usually with a lot of irrelevant noise in it. The work is shrinking it to the minimum reproducing case, then asking which assumption it violated. Frequently the answer is that the invariant was wrong rather than the code, and that is still a finding: it means the specification and the implementation disagreed about what the system guarantees.

Where it sits in an audit

We write invariants during the threat-modelling phase, before the manual review, because the act of writing them forces the protocol's guarantees to be stated explicitly. Teams are often unable to articulate their own invariants on the first attempt, and that conversation alone has surfaced design problems before a line of the review was done.

Those same properties are what our monitoring runs against after launch. A property worth testing once is worth testing every block.

Working on something in this area? Tell us about it.