cc @Untitled Contact @Untitled Contact @Untitled Contact @Untitled Contact @Untitled Contact

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.