Inductive Invariants Over Reachable States

Every non-trivial system has properties that must hold in all states it can actually reach, not merely in the states the designer happened to test. “The sum of all account balances equals the ledger total” is such a property. So is “no order is marked shipped before payment is captured”. These are invariants, and the standard way to establish one is induction over the execution steps.

The induction is easy to state and hard to apply. A property $I$ is an invariant of a system with initial states $S_0$ and transition relation $T$ when (1) $I$ holds in every state of $S_0$, and (2) for every pair of states $(s, s’)$ with $T(s, s’)$, $I(s)$ implies $I(s’)$. Those two obligations are the base case and the step case. When both hold, $I$ holds in every reachable state, by induction on the length of the execution prefix.

The catch is that most properties of interest do not satisfy obligation (2) on their own. The step case fails, not because the property is false, but because the induction hypothesis is too weak: knowing $I$ at one state is not enough to conclude $I$ at the next. The remedy is to strengthen $I$ until the step case goes through. That strengthening is the entire craft, and it is where specifications acquire most of their auxiliary clauses.

The step case fails for a reason worth reading

Consider a queue with a fixed capacity and a producer that may only enqueue when the length is below capacity. The property “length $\le$ capacity” holds initially at length zero, and the enqueue transition preserves it by construction: the guard is precisely the negation of the violation. The step case succeeds because the guard carries the information the proof needs.

Now remove the guard and let the producer enqueue unconditionally, with a consumer that dequeues. The property “length $\le$ capacity” is still true of the intended system, but it is not inductive: from a state where length equals capacity, the unguarded enqueue produces a state that violates it. No amount of reasoning recovers the property, because the system as specified does not have it. The proof failure is a specification defect, and it is exactly the defect a reviewer would have missed while reading the transition list.

The subtler case is a property that is true but not inductive because the transition relation loses information. Take a bank transfer between two accounts, where the invariant is that the total is unchanged. The transition subtracts from one account and adds to the other. If the two updates are separate steps, the intermediate state has the total reduced by the transferred amount, so the property fails at the midpoint even though the end state satisfies it. The property is true of every completed transfer and false of every state between the two halves.

The repair is either to make the transfer atomic in the model — one transition, two effects — or to strengthen the invariant to something that is preserved by each half, such as “total plus the sum of in-flight amounts is unchanged”. The second option is what an implementation of a non-atomic transfer actually relies on, and it is why real systems carry an explicit in-flight ledger rather than trusting the two updates to pair up. The strengthened invariant is not an artefact of the proof; it names a piece of state the design needs.

Strengthening, and how to find the missing conjunct

When the step case fails, the counterexample is a pair of states: one satisfying $I$, one not, connected by a transition. Reading that pair backwards usually names the missing conjunct. In the transfer case, the counterexample state has the total reduced and no record of an outstanding transfer, so the missing conjunct is precisely “the difference is accounted for by in-flight operations”.

Three heuristics cover most cases. The first is to add the negation of every reachable bad state as a conjunct, then generalise it into a condition over the variables rather than over specific values. The second is to add a type or range constraint on each variable — invariants rarely hold without the bounds that the implementation enforces elsewhere. The third is to add relational facts between variables that the transitions maintain but that no single transition states: a counter equal to the length of a list, a version number monotone in a sequence, a flag that is set if and only if a field is non-null.

That third category is where the real information lives. A specification that declares status and shipped_at as independent fields has no invariant connecting them, and any implementation that sets one without the other is consistent with the document. Adding the invariant status = shipped iff shipped_at is present converts a convention into a requirement, and makes the pair of fields a single piece of state with two projections. This is the same reduction that makes state machine specifications analysable: extra variables that are functions of the declared state add no reachable states, but they do add proof obligations.

Invariants versus inductive invariants

The distinction is worth stating precisely, because it is frequently blurred. An invariant is any property true of all reachable states. An inductive invariant is a property that satisfies both obligations, and therefore proves itself true of all reachable states without further argument.

Every inductive invariant is an invariant. The converse fails, and the failure is not exotic: for most systems, the strongest property one can write down directly — the set of reachable states itself — is inductive, but it is not expressible in the specification language. The practical consequence is that a proof of safety is always a proof about some over-approximation. The strengthened $I$ admits states that the system cannot reach; it merely admits no transition that escapes it. That is fine for safety, since safety is a statement about all reachable states and a property holding on a superset holds on the subset.

It is not fine for the reverse direction. If a property is proved over an over-approximation, the proof may succeed on states that no execution reaches, which is harmless, but it may also fail on such states, which is a false alarm. Refining the model to remove unreachable states is how false alarms are eliminated, and it is why model checkers spend most of their effort on reachability rather than on the property.

What the obligations cost in practice

Writing an inductive invariant for a specification with $n$ variables and a transition relation of $m$ guarded actions produces $m$ verification conditions, each of the form “guard and $I$ imply $I’$”. For a specification of realistic size, $m$ is in the tens and each condition is a formula over the state variables, often with quantifiers over collections.

Two costs follow. The first is that the conditions are only as strong as the model. An unconstrained variable — one whose type is an unbounded integer, or a collection with no size limit — makes some conditions unprovable without additional assumptions, and the assumptions become part of the specification. A specification that says “the queue holds at most 1000 items” is not a comment on the implementation; it is a constraint the proof needs.

The second is that invariants must be maintained as the model changes. Adding a transition adds a condition, and the added transition is exactly the one most likely to break an existing conjunct, because the conjunct was written without it in mind. This is the ordinary maintenance problem of specifications, and it argues for keeping the invariant set small and each conjunct justified by a named requirement rather than by convenience.

The discipline that survives is unglamorous: state the invariant before the transitions, derive the guards from it where possible, and treat any transition that cannot preserve it as evidence that either the guard or the invariant is wrong. A system whose safety argument consists of one sentence that is checked against every action is easier to change than one whose safety argument is a paragraph of prose that nobody re-reads. The same structure reappears at the level of whole-system behaviour in liveness and fairness properties, where the induction is over infinite executions and the obligations change shape.