How to Write Inductive Invariants
This post is about a method that will allow you to deepen the understanding of protocols and concurrent systems. Quint recently added a command line argument called --inductive-invariant. The term “inductive invariant” is scary, but we like them, as they allow us to prove the absence of design bugs in distributed systems. Moreover, the act of writing an inductive invariant is a great tool that allows you to learn how to think about distributed systems. Before diving into the tutorial part, let’s discuss what is going on here.
Like in all relevant areas in distributed systems, there is a great paper by Leslie Lamport on this. Reading it can be quite intimidating: read it only if you are very self-confident as an engineer. We suggest you continue with this post first before you read Lamport’s paper .
The notion of a “correct state” is super important, and we will come back to it a lot in this text. If you want to build confidence that your system is doing the right thing, you need to demonstrate that it “maintains a correct state”. Surprisingly, “maintains” is the easy part here. It just means executing your protocol. Put simply, you take an arbitrary correct state, you let your protocol do a step, and you end up in another correct state. We know what taking a step means: it is defined by the program code or by your actions defined in Quint. This is clear. But what is “a correct state”? Well, let’s say that the initial state is correct. But then? This is surprisingly hard.
