In Leslie Lamport's view, an invariant is a property of a system that must remain true in every reachable state of its execution.
Invariants are fundamental to Lamport's approach to distributed systems, particularly in TLA+ (Temporal Logic of Actions).
1. What is an invariant?
Imagine a distributed system as a sequence of states:
A system evolves through actions that change its state.
An invariant is a condition P such that:
For example, in a bank:
If the system guarantees that no account can have a negative balance, this property must hold regardless of the sequence or interleaving of operations.
2. Invariants versus other properties
Lamport distinguishes between two important kinds of properties.
Property | Meaning | Example |
|---|---|---|
Safety | Something bad never happens | Two actors never own the same exclusive lock |
Liveness | Something good eventually happens | A submitted transaction eventually completes |
An invariant is a state-based safety property.
A classic distinction is that safety is about never violating a rule, whereas liveness is about eventually making progress.
Not all safety properties are directly expressible as invariants over the original state variables; sometimes auxiliary history variables are needed.
3. How Lamport proves invariants
Lamport uses inductive reasoning.
To prove an inductive invariant, establish two things:
Initialization: The invariant holds in every initial state.
Preservation: Every valid transition preserves the invariant.
Formally:
Here, Inv' refers to the invariant evaluated in the next state.
An important subtlety: a property can be an invariant without being inductive itself. In that case, you can use a stronger inductive invariant to prove it.
4. Example: Invariants in Seed's distributed objects
Consider a distributed document replicated across multiple devices.
Possible invariants include:
Invariant | What must always be true |
|---|---|
Identity integrity | Every accepted change has a valid author signature |
Causal integrity | Every applied change has its required dependencies |
Version integrity | A change identifier always refers to the same immutable change |
Authorization | Every accepted operation satisfies the applicable authorization policy |
DAG integrity | The change-dependency graph contains no cycles |
These are candidate invariants: their precise definitions depend on your system's state model and trust assumptions.
For example, with concurrent edits, different replicas can have different document states without violating an invariant.
That's an important distinction:
An invariant does not mean that the state never changes, or that all replicas have identical states. It means that certain properties remain true despite all permitted changes.
Furthermore, eventual convergence is not itself a simple state invariant. It is a property about how executions evolve over time under appropriate assumptions.
5. Why this matters for distributed systems
Lamport's approach is to specify what a system must guarantee before deciding how to implement it.
Rather than asking only:
How should my distributed object process messages?
Ask:
What properties must remain true regardless of message ordering, concurrency, or failures?
Then design the object's state transitions to preserve those properties.
This connects directly to your recent questions about the Actor Model and state machines: a state machine defines possible transitions; invariants constrain the states those transitions may reach.
For a deeper introduction, see Lamport's Proving Safety Properties.
The most important idea is that invariants define what must never become false, even when everything else in the system is changing.
Do you like what you are reading? Subscribe to receive updates.
Unsubscribe anytime