We’ve proven our light switch works. Now what?
In Part 13 🐞, we introduced formal verification — the idea of proving system correctness using math and models.
We showed how to model a simple system (a light switch) using Quint, and how to check that certain things never go wrong.
But what kinds of things are we checking, really?
Let’s talk about the one of the big property type in formal methods:
Safety property: “Nothing Bad Ever Happens”
Safety properties are about ruling out bad outcomes.
They say: “this should never happen.”
If a safety property is violated, the model checker will show you a specific step where the system breaks that rule.
Classic examples:
- “Two threads are never in the critical section at the same time.”
- “A bank account balance never goes negative.”
- “A file is never deleted without confirmation.”
- “The light is never both on and off.”
These properties are often written as invariants — they must hold in every reachable state.
In Quint :
Once violated, safety can’t be recovered. That’s what makes it sharp — and easy to reason about.
🧱 Example: Detecting Deadlock
Let’s say you have two processes competing for two shared resources. Each process can acquire or release either resource. If one grabs R1 and the other grabs R2, and both are waiting on the other — we have a deadlock.
Here’s how we model that in Quint:
module DeadlockSimple {
val P1: int = 1
val P2: int = 2
// heldBy = (owner of R1, owner of R2); -1 means free
var heldBy: (int, int)
// Initially, both resources are free
action init = heldBy' = (-1, -1)
// Use nondet properly to select `p` and `nextHeld`
action step = {
nondet p = oneOf(Set(P1, P2))
nondet nextHeld = oneOf(Set(
// Try to acquire R1
if (heldBy._1 == -1) (p, heldBy._2) else heldBy,
// Try to acquire R2
if (heldBy._2 == -1) (heldBy._1, p) else heldBy,
// Try to release R1
if (heldBy._1 == p) (-1, heldBy._2) else heldBy,
// Try to release R2
if (heldBy._2 == p) (heldBy._1, -1) else heldBy
))
heldBy' = nextHeld
}
// Deadlock: both resources held by different processes
def deadlock: bool =
and {
heldBy._1 != -1,
heldBy._2 != -1,
heldBy._1 != heldBy._2
}
// SAFETY: No deadlock allowed
val NoDeadlock = not(deadlock)
}
We define NoDeadlock as a safety property — the system should never reach a state where each process holds one resource and waits for the other. When we check it (either simulation or verification would violate the property but for now we would use the simulation):
quint run DeadlockSimple.qnt --invariant=NoDeadlock --verbosity=5
We get this output:
[Frame 0]
q::initAndInvariant => true
└─ init => true
[State 0] { heldBy: (-1, -1) }
[Frame 1]
q::stepAndInvariant => true
└─ step => true
[State 1] { heldBy: (-1, -1) }
[Frame 2]
q::stepAndInvariant => true
└─ step => true
[State 2] { heldBy: (-1, 1) }
[Frame 3]
q::stepAndInvariant => false
└─ step => true
[State 3] { heldBy: (2, 1) }
[violation] Found an issue (5ms).
Use --verbosity=3 to show executions.
Use --seed=0x2cb19ed597be9 to reproduce.
error: Invariant violated
Boom 💥 — the model checker found a deadlock scenario:
- P1 grabs R2
- P2 grabs R1
- Neither can proceed
This is the beauty of safety properties:
If something bad can happen, the model checker shows exactly how.
✅ Fixing the Deadlock: Ordered Acquisition
Now as we detected our bug within our specification, we need to solve that. One way how to do it, is to introduce simple strategy (i.e, resource ordering).
Every process must acquire R1 before attempting R2.
This guarantees that both won’t end up waiting on each other in a circular dependency. Here’s the updated, deadlock-free version of our model:
module DeadlockFixed {
val P1: int = 1
val P2: int = 2
// heldBy = (R1 owner, R2 owner); -1 = free
var heldBy: (int, int)
// Both resources are free initially
action init = heldBy' = (-1, -1)
// Each process follows resource acquisition order: R1 → R2 → release all
action step = {
nondet p = oneOf(Set(P1, P2))
nondet nextHeld = oneOf(Set(
// Acquire R1 (only if free)
if (heldBy._1 == -1) (p, heldBy._2) else heldBy,
// Acquire R2 only if R1 already held by same process and R2 is free
if (heldBy._1 == p and heldBy._2 == -1) (heldBy._1, p) else heldBy,
// Release R2
if (heldBy._2 == p) (heldBy._1, -1) else heldBy,
// Release R1 (only after releasing R2)
if (heldBy._2 != p and heldBy._1 == p) (-1, heldBy._2) else heldBy
))
heldBy' = nextHeld
}
// Deadlock = both resources held by different processes
def deadlock: bool =
and {
heldBy._1 != -1,
heldBy._2 != -1,
heldBy._1 != heldBy._2
}
val NoDeadlock = not(deadlock)
}
Now run the model checker again:
quint verify DeadlockFixed.qnt --invariant=NoDeadlock
And you’ll see in case of simulation:
[ok] No violation found (1522ms).
or verification using Apalache model-checker:
The outcome is: NoError I@16:12:38.422
[ok] No violation found (2457ms).
We can see the simulation trace without Deadlock:
quint run DeadlockFixed.qnt --invariant=NoDeadlock --verbosity=5
An example execution:
[Frame 0]
q::initAndInvariant => true
└─ init => true
[State 0] { heldBy: (-1, -1) }
[Frame 1]
q::stepAndInvariant => true
└─ step => true
[State 1] { heldBy: (1, -1) }
[Frame 2]
q::stepAndInvariant => true
└─ step => true
[State 2] { heldBy: (1, -1) }
[Frame 3]
q::stepAndInvariant => true
└─ step => true
[State 3] { heldBy: (1, 1) }
[Frame 4]
q::stepAndInvariant => true
└─ step => true
[State 4] { heldBy: (1, 1) }
[Frame 5]
q::stepAndInvariant => true
└─ step => true
[State 5] { heldBy: (1, -1) }
[Frame 6]
q::stepAndInvariant => true
└─ step => true
[State 6] { heldBy: (-1, -1) }
[Frame 7]
q::stepAndInvariant => true
└─ step => true
[State 7] { heldBy: (1, -1) }
[Frame 8]
q::stepAndInvariant => true
└─ step => true
[State 8] { heldBy: (1, -1) }
[Frame 9]
q::stepAndInvariant => true
└─ step => true
[State 9] { heldBy: (1, -1) }
[Frame 10]
q::stepAndInvariant => true
└─ step => true
[State 10] { heldBy: (1, -1) }
[Frame 11]
q::stepAndInvariant => true
└─ step => true
[State 11] { heldBy: (1, 1) }
[Frame 12]
q::stepAndInvariant => true
└─ step => true
[State 12] { heldBy: (1, -1) }
[Frame 13]
q::stepAndInvariant => true
└─ step => true
[State 13] { heldBy: (1, -1) }
[Frame 14]
q::stepAndInvariant => true
└─ step => true
[State 14] { heldBy: (1, -1) }
[Frame 15]
q::stepAndInvariant => true
└─ step => true
[State 15] { heldBy: (1, -1) }
[Frame 16]
q::stepAndInvariant => true
└─ step => true
[State 16] { heldBy: (1, -1) }
[Frame 17]
q::stepAndInvariant => true
└─ step => true
[State 17] { heldBy: (1, -1) }
[Frame 18]
q::stepAndInvariant => true
└─ step => true
[State 18] { heldBy: (1, -1) }
[Frame 19]
q::stepAndInvariant => true
└─ step => true
[State 19] { heldBy: (1, -1) }
[Frame 20]
q::stepAndInvariant => true
└─ step => true
[State 20] { heldBy: (1, -1) }
[ok] No violation found (1822ms).
This is not just luck — it’s a direct result of the design. By enforcing ordered acquisition, we eliminated one of the four Coffman conditions for deadlock (specifically, circular wait).
🍝 Example: Dining Philosophers with Safety Guarantees
The classic Dining Philosophers problem is often used to model resource sharing and synchronization. Philosophers sit around a table with one fork between each of them. To eat, a philosopher needs both the left and right forks.
In this Quint model, we ensure that:
- Forks are acquired in pairs
- Philosophers can’t eat at the same time as their neighbors
- No fork is held by more than one philosopher
You can explore the full model here.
🔒 Defining Safety in Quint:
We express the safety guarantees as invariants — properties that must hold in every state of the system. For example:
val TypeOk = and {
// All forks must be valid fork IDs
forks.subseteq(philosophers.map(leftFork).union(philosophers.map(rightFork))),
// Each taken pair must include a valid philosopher and a currently held fork
taken.forall(pair => pair._1.in(philosophers) and pair._2.in(forks))
}
And the main safety condition:
val Safety = and {
// No two neighboring philosophers are eating at the same time
philosophers.forall(p =>
not(states.get(p) == Eating and states.get(rightPhilosopher(p)) == Eating)
),
// Mutual exclusion: Each fork is held by at most one philosopher
forks.forall(f =>
size(taken.filter(pair => pair._2 == f)) <= 1
)
}
This combined Safety invariant actually encodes two distinct properties:
- No neighbor conflict — adjacent philosophers can’t eat simultaneously
- Mutual exclusion on forks — each fork has at most one holder
You could easily split these into separate invariants (e.g., NoNeighborConflict and MutualExclusion) to verify them independently — but here, we’ve bundled them under a single name for convenience.
✅ Checking the Invariants
To verify the system is safe under all possible execution paths, simply run:
quint verify DiningPhilosophersDeadlockFree5.qnt --invariant=Safety
The model checker will explore the entire state space and confirm that the system never violates our invariant — even under arbitrary interleavings. If you’d like to inspect the execution trace, you can also simulate it:
quint run DiningPhilosophersDeadlockFree5.qnt --invariant=Safety --max-steps=100
🧩 Wrapping Up: Why Safety Matters
Safety properties are often the first line of defense in system correctness — and for good reason:
- They are precise, binary, and local: either something bad can happen, or it can’t.
- They are easy to explain to engineers, designers, and stakeholders.
- They catch some of the most catastrophic issues — like deadlocks, race conditions, and violations of mutual exclusion — at the design stage.
What’s powerful is not just that we detect problems, but that we can prove they’re impossible by construction.
In the next post, we’ll go beyond “nothing bad happens,” and explore liveness and fairness:
- How do we prove that something good eventually happens?
- How do we make sure progress isn’t just possible, but inevitable?
Until then: stay… you know the word :P –> safe🛡.️