*Note: to understand this post, it helps to have some familiarity with TLA+. *

Leslie Lamport is a big advocate of *inductive invariants.* In Teaching Concurrency, he introduces the following simple concurrent algorithm:

*Consider N processes numbered from 0 through N−1 in which each process i executes:*

`x[i] := 1;`

`y[i] := x[(i−1) mod N]`

*and stops, where each x[i] initially equals 0.*

Lamport continues:

This algorithm satisfies the following property: after every process has stopped,

y[i]equals 1 for at least one processi.…

The algorithm satisfies this property because it maintains an

inductive invariant[emphasis added]. Do you know what that invariant is? If not, then you do not completely understand why the algorithm satisfies this property. How can a computer engineer design a correct concurrent system without understanding it?

Before I read up on TLA+, I was familiar with the idea of an *invariant*, a property that is always true throughout the execution of a program. But I didn’t know what an inductive invariant is.

## Mathematical induction

An inductive invariant of a specification is an invariant you can prove using mathematical induction. You probably had to do proofs by induction in college or high school math.

To refresh your memory, let’s say you were asked to prove the following formula:

The way this is proved this by induction is:

- Base case: Prove it for n=1
- Inductive case: Assume it is true for n, and prove that it holds for n+1

In TLA+, you typically specify the allowed behaviors of a specification by writing two predicates:

- The initial conditions, conventionally written as
*Init* - The allowed state transitions (which are called
*steps*in TLA+), conventionally written as*Next*

Let’s say we have a state predicate which we believe is an inductive invariant, which I’ll call *Inv*. To prove that *Inv* is an inductive invariant, you need to:

- Base case: Prove that
*Inv*is true when*Init*is true - Inductive case: Assume that
*Inv*holds for an arbitrary state*s*, prove that*Inv*holds for an arbitrary state*t*where the*step**s→t*is one of the state transitions permitted by*Next*.

In TLA+ syntax, the top-level structured proof of an inductive invariant looks like this:

THEOREM Spec=>[]Inv

<1>1. Init => Inv

<1>2. Inv /\ [Next]_vars => Inv'

<1>3. QED

BY <1>1,<1>2

In practice, you want to prove some invariant that is not an inductive invariant. The proof is typically structured like this:

Correct = ... \* The invariant you really want to prove

Inv = ... /\ Correct \* the inductive invariant

THEOREM Spec=>[]Correct

<1>1. Init => Inv

<1>2. Inv /\ [Next]_vars => Inv'

<1>3. Inv => Correct

<1>4. QED

BY <1>1, <1>2, <1>3

## Not all invariants are inductive

If you’re using TLA+ to check the behavior of a system, you’ll have an invariant that you want to check, often referred to as a *correctness* property or a *safety* property. However, not all such invariants are inductive invariants. They usually aren’t.

As an example, here’s a simple algorithm that starts a counter at either 1 or 2, and then decrements it until it reaches 0. The algorithm is written in PlusCal notation.

--algorithm Decrement

variable i \in {1, 2};

begin

Outer:

while i>0 do

Inner:

i := i-1;

end while

end algorithm

It should be obvious that *i≥0* is an invariant of this specification. Let’s call it *Inv.* But *Inv* isn’t an inductive invariant. To understand why, consider the following program state:

pc="Inner"

i=0

Here, *Inv * is true, but *Inv’ *is false, because on the next step of the behavior, *i* will be decremented to -1.

Consider the above diagram, which is associated associated with some TLA+ specification (not the one described above). A bubble represents a state in TLA+. A bubble is colored gray if it is an initial state in the specification (i.e. if the *Init* predicate is true of that state). An arrow represents a step, where the *Next* action is true for the pair of states associated with the arrow.

The inner region shows all of the states that are in all allowed behaviors of

a specification. The outer region represents an invariant: it contains all states where the invariant holds. The middle region represents an inductive invariant: it contains all states where an inductive invariant holds.

Note how there is an arrow from a state where the invariant holds to a state

where the invariant doesn’t hold. That’s because invariants are not inductive in general.

In contrast, for states where the inductive invariant holds, all arrows that

start in those states terminate in states where the inductive invariant holds.

## Finding an inductive invariant

The hardest part of proof by inductive invariance is finding the inductive invariant for your specification. If the invariant you come up with isn’t inductive, you won’t be able to prove it by induction.

You can use TLC to help find an inductive invariant. See Using TLC to Check Inductive Invariance for more details.

## I want to learn more!

The TLA+ Hyperbook has a section called *The TLA+ Proof Track* about how to write proofs in TLA+ that can be checked mechanically using TLAPS.

I’ve only dabbled in writing proofs. Here are two that I’ve written that were checked by TLAPS, if you’re looking for simple examples:

- The “Teaching Concurrency” algorithm mentioned earlier
- Leftpad as part of Hillel Wayne’s Let’s prove leftpad challenge

Interesting post! Finding the right inductive invariants are indeed the hardest part of some proofs, and it’s often a delicate (and pleasing) balancing act to find one that’s weak enough to be provable whilst being strong enough to give you the desired conclusion at the end. It normally takes me many iterations to get it right, and I have definitely got better at this with practice.

The invariant in your TLA+ file [1] feels quite odd to me, particularly that the `AtLeastOneYWhenDone` clause is sufficient. It seems too weak. It is quite rare to be able to use an invariant that only carries any weight at one state (termination), and more usual to use an invariant to carry some fact about the system across multiple states. That’s not to say it doesn’t work (it certainly does, see [2]) so much as to say that the invariant I arrived at for this algorithm is quite different [3], effectively saying:

(∀n < N. y[n] is defined ⟶ x[n] = 1) ∧ ((∀n < N. x[n] = 1) ⟶ (∃ n < N. y[n] is undefined ∨ y[n] = 1))

This works as well, and it's interesting to see a situation where there's a choice of satisfactory invariants.

[1] https://github.com/lorin/teaching-concurrency/blob/d44b4cf2e360afadebb366b34cb7cbbaa2ebffc5/Simple.tla#L68-L70

[2] https://github.com/DaveCTurner/tla-examples/blob/bd66616d05445434c67a1342485ba4d7bfebf3e3/HochsteinLamport.thy#L267

[3] https://github.com/DaveCTurner/tla-examples/blob/6f27f9f79f1798eb6873dee9161187053b984a5b/HochsteinLamport.thy#L56-L61

I have the `AtLeastOneYWhenDone` clause in my inductive invariant because I’m following Lamport’s advice of conjoining the safety property you’re trying to prove to your inductive invariant. Doing so makes it trivial to do the final step in the proof [1]

Inv ⟶ AtLeastOneYWhenDone

(I know it sounds odd to call a predicate an “invariant” when it’s vacuously true except for one state). It might not strictly be necessary here, I haven’t tried doing the proof without that clause in the invariant.

I should really learn Isabelle/HOL so I can read your proofs!

[1] https://github.com/lorin/teaching-concurrency/blob/d44b4cf2e360afadebb366b34cb7cbbaa2ebffc5/Simple.tla#L107