We proved nothing bad ever happens. But does anything good ever happen?

In Part 14, we explored safety properties: those that make sure our system doesn’t enter a bad state. But what about the opposite?

What if we want to ensure that:

• A message is eventually delivered
• A file is eventually replicated
• A philosopher eventually eats

These are liveness properties.

⏳ What is Liveness?

Liveness properties capture the idea of progress. They say:

“Something good will eventually happen.”

Unlike safety (where one bad state breaks the guarantee), liveness can’t be violated in a single step. It’s only violated if the good thing never happens — no matter how long we wait.

Examples of Liveness:

• “Every request eventually gets a response”
• “Every lock is eventually released”
• “Every philosopher eventually gets to eat”

Liveness vs Safety (basic overview)

⌚ Temporal Logic: Reasoning Over Time

Classical logic — using predicates like x > 0 or isLocked = false — is powerful, but it’s fundamentally timeless. It tells us what is true now, in a single instant. But systems don’t just exist in the now — they evolve. They move from state to state.

This is especially true in concurrent or distributed systems, where behavior spans across time: requests are sent and later responded to, locks are acquired and eventually released, messages are delivered (hopefully) eventually.

To reason about these systems, we need a richer logic — one that understands time. That’s where temporal logic comes in. It allows us to describe not just what must be true, but when it must be true.

⏳ Temporal Logic Operators (in LTL)

These operators allow us to describe how a system behaves across all possible executions over time. There are many more temporal logics like Computation Tree Logic (CTL), which has branching timelines (many futures) instead of one linear line of time. Moreover, it adds path quantifiers (i.e., A = “for all futures” andE = “there exists a future”). So one could create temporal property “On all paths, if hungry, then eventually eating”, which can be written as AG (hungry → AF eat). Furthermore, we also know CTL* which is superset of both LTL and CTL and can freely combine path quantifiers and temporal operators But in my personal practice I met with mostly LTL logic.

🌟 Temporal Logic in TLA+ and Quint

TLA+

• TLA+ uses [] (always) and <> (eventually)
• Mixes state predicates (what’s true now) and actions (what can change)
• Example:

  [] (x < 10)       // Always true
  <> (x = 42)       // Eventually x becomes 42
  []<>(x = 0)       // Infinitely often, x = 0
  

Quint

• Quint supports always, eventually and more which I assume maps to TLA+ operators (i.e., [], <>, …)
• Temporal formulas can be used directly in the model:

  temporal Liveness = always(eventually(x == 42))
  temporal Liveness2 = x == 0 leadsTo x == 1
  

Fairness plays a critical role in verifying liveness properties. Without fairness, a model checker might find counterexamples where an action is enabled forever but simply never chosen — an unrealistic execution that violates liveness only because of unfair scheduling.

Fairness assumptions help rule out such pathological behaviors:

• Weak fairness says: if an action is continuously enabled, it must eventually occur.
• Strong fairness says: if an action is enabled infinitely often, it must eventually occur.

These assumptions let us model real-world schedulers more accurately, where starvation is not tolerated.

🔌 A Minimal Liveness Example (with Fairness)

Let’s go back to our trusty Light Switch model.

var isOn: bool

action init = all { isOn' = false }
action turnOn = all { isOn' = true }
action turnOff = all { isOn' = false }
action step = any { turnOn, turnOff }

Without fairness, the system might stutter forever in the same state.

Liveness Without Fairness

temporal Liveness = always(eventually(isOn))

This might fail! If the system just never chooses turnOn, isOn never becomes true.

Weak Fairness to the Rescue

temporal WeakFairStep = weakFair(step, isOn)
temporal WeakLiveness = WeakFairStep implies always(eventually(isOn))

Now if step is always enabled, it must eventually happen — and the light must turn on.

Strong Fairness

To ensure toggling on/off forever:

temporal StrongFairStep =
  strongFair(turnOn, isOn) and strongFair(turnOff, isOn)

// Liveness: light toggles forever
temporal StrongLiveness =
  StrongFairStep implies always(eventually(isOn and eventually(not(isOn))))

If interest in the whole Light Switch Quint specification check this.

☕ Example: Dining Philosophers & Starvation

In the Dining Philosophers model:

We define deadlock as a state where all philosophers are hungry but no one can pick up forks.

temporal DeadlockProperty = eventually(deadlockCondition)

To ensure the system never gets stuck, we use fairness:

temporal DeadlockFreedom = weakFair(step, vars) implies always(eventually(not(deadlockCondition)))

Want more? We can even define starvation freedom:

temporal StarvationFreedom = weakFair(step, vars) implies philosophers.forall(p => eventually(states.get(p) == Eating))

Closing thoughts…

Firstly, let’s recap what we’ve learned in this blog post:

• Safety ensures that nothing bad ever happens — your system stays within well-defined boundaries.
• Liveness guarantees that something good eventually happens — your system doesn’t just sit there; it progresses.
• Fairness helps unlock liveness by ensuring that enabled actions aren’t indefinitely ignored — preventing starvation and ensuring opportunity.

Together, they form a complete picture of correctness over time.
And temporal logic gives us the language to express these ideas with mathematical precision.
Tools like Quint let us turn these ideas into executable specifications we can simulate, verify, and reason about — before writing any code.

In the next post, we’ll explore model-based testing with Quint — a powerful way to bridge the gap between your specification and your implementation. We’ll see how Quint models can become more than just proofs of correctness — they can drive the generation of test cases, uncover edge cases, and keep your implementation in sync with your design. Because in real-world systems, correctness isn’t just about being safe — it’s about staying aligned over time.

Until then, may your systems be not just correct… but eventually correct. ✨