Invariants & properties
Stage 4 of the verification model is where Faultbox decides whether a run is healthy. It does that by checking properties against the event log. This page explains what a property is, the three kinds you’ll write, and how to find the ones that matter — the question every team gets stuck on.
A test checks a case; an invariant checks a truth
A test says: “when X happens, Y should be the result.” It covers one scenario under one fault. It only catches the cases you thought to write.
An invariant is stronger: “Y must be true no matter what happens.” It is not tied to a scenario — it is evaluated in every cell of the matrix, under every fault, in every explored ordering. If any leaf violates it, you have found a real bug, even in a combination you never explicitly considered.
A test is a spot-check. An invariant is a net stretched under the whole matrix. Distributed-system bugs fall into the gaps between spot-checks; the net is what catches them.
The two fundamental kinds: safety and liveness
Formal verification splits properties in two. The split is practical, not academic — it tells you which Faultbox primitive to reach for.
Safety — “bad things never happen”
A safety property is violated at an exact instant you can point to.
| System | Safety property | Violation |
|---|---|---|
| Inventory | stock >= 0 always | stock = −1 at time T |
| Banking | sum(balances) is constant | the sum changed |
| Orders | each order_id appears once | a duplicate appeared |
| Durability | confirmed ⇒ persisted | confirmed, but no DB row |
Encode with: assert_never(...) and monitor() state machines that
fail() on violation.
Liveness — “good things eventually happen”
A liveness property is violated only by waiting long enough and seeing nothing. The system got stuck.
| System | Liveness property | Violation |
|---|---|---|
| Queue | every message is eventually consumed | message sits forever |
| Retries | a failed write is eventually retried | no retry after the deadline |
| Circuit breaker | eventually closes again | stays open permanently |
Encode with: eventually(...), await_event(...), await_stable(...).
Safety without liveness is a system that never does anything wrong because it never does anything. Liveness without safety is a system that eventually finishes — having corrupted your data on the way. You need both.
Temporal properties — the third dimension: when
Safety and liveness are about whether. Temporal properties add when and in what order — the dimension where the nastiest distributed bugs hide. Faultbox gives you four temporal operators plus stateful monitors:
| Operator | Reads as | Catches |
|---|---|---|
eventually(p) | ”p becomes true at some point” | liveness — did it ever finish? |
always(p, between=(a,b)) | ”p holds the whole time between a and b” | a guarantee that must not lapse mid-flight |
await_event(matcher) | ”block until this event, or time out” | ordering / synchronization points |
await_stable(quiescence_window=...) | ”wait until the system goes quiet" | "did it settle, or is it still thrashing?” |
And for properties with memory — counts, sequences, before/after — a
monitor() is a small state machine over the event stream:
monitor("at_most_one_publish",
on = lambda e: e["type"] == "topic" and e.get("topic") == "order-events",
state_init = {"count": 0},
update = lambda st, e: {"count": st["count"] + 1},
check = lambda st: st["count"] <= 1 or fail("duplicate publish"),
)A monitor travels with the failure mode: attach it to a fault_assumption
via monitors=, and every matrix cell that uses that assumption checks it
automatically. You wire invariants per failure mode, not per test — a new
scenario added to the matrix inherits the whole safety net for free.
Detailed patterns (before/after, count constraints, orphan-event detection, data-integrity checks) live in the how-to guide. This page is about what the property is; the guide is about how to write each shape.
→ Do it: Find & encode invariants
How to find invariants
This is the part teams find hard. Four reliable techniques:
1. Follow the money
For any system holding valuable state (money, orders, inventory, seats), trace
the lifecycle — created → processing → committed → confirmed — and at each
transition ask: can it go backwards (safety)? can it get stuck (liveness)?
can it skip a step (safety)? can two transitions happen at once (concurrency)?
2. Read your own error handling
Your existing error handling already states invariants implicitly:
if err := db.Insert(order); err != nil {
return fmt.Errorf("not persisted: %w", err) // ← invariant: no publish without a successful insert
}
kafka.Publish("order-created", order)The code assumes “if Insert fails, don’t publish.” That assumption is the invariant — “no Kafka event without a committed DB row.” Make it explicit as a monitor, then break the insert with a fault and watch whether the code keeps its own promise.
3. Mine production incidents
Every incident is a violated invariant in hindsight. “Orders were duplicated” → a uniqueness invariant. After each incident: name the property that broke, write the fault that reproduces it, attach the monitor. This turns one-time pain into permanent protection.
4. Ask “what if both at once?”
For any pair of operations: two orders for the last item (oversell?), a write
racing a read (stale read?), a retry racing the original (double-process?).
These become parallel() scenarios explored across
interleavings.
Where properties produce verdicts
A property check has three outcomes, not two — which is why Faultbox verdicts are three-valued:
- holds → contributes to PASS
- violated → FAIL (with the offending event and the leaf’s seed)
- never exercised → INCONCLUSIVE — the fault never fired, or the system never reached the checked state, so the property was neither confirmed nor refuted. A silent green here would be a lie.
→ Concept: Reading reports & verdicts
Next: The fault matrix & exploration → — how Faultbox provokes the failures these properties are checked against.