Most of jaque's guarantees are stated as invariants and checked mechanically, not asserted in prose. Status says what is shipped; this page says why the marks there can be trusted, and what the checks found on the way.

1. The handover between engines is model-checked

When several engines share one event log, each object has exactly one owner at a time, and ownership moves when an engine joins, leaves or loses its heartbeat. The rules that make that safe are written as a TLA+ specification: engines, a shared log, a membership store, one owner per object per membership view, every write stamped with the writer's epoch, and readers that ignore anything older than the last thing they folded.

The invariant is the one the cluster page promises: two live engines whose view is current and whose tail is at the end of the log never disagree on an object's state. The checker exhausts every interleaving of a two-engine cluster, writes, membership changes, partitions, restarts and replays, over seventeen million states, and reports that the invariant holds.

1.1 What it found first

The specification was written against the rules the code shipped with, and the checker broke them twice before it passed:

• A seven-step sequence with no network partition at all. The previous owner writes its last record and leaves. The new owner refreshes its view first, then reads that record and ignores it, because the object is "owned now" and owned records were treated as its own. The new owner starts from a stale state.
• An eleven-step sequence. An engine has already seen a newer epoch for an object on the log and still writes it under the view it had.

Both sequences are now regression tests, replayed over two real engines sharing one log. Both were red before the rules changed and green after: an engine ignores only the records it wrote itself, and an engine that has seen the log outrun its view does not write until its view catches up. The code is bound to exactly the configuration of the model that holds.

1.2 Every verdict is pinned

Five configurations of the model are checked, and each declares the verdict it must produce: the rules as first shipped (violated), read-side rules only (violated), the rules the code runs (holds), a variant that folds everything at the tail (holds), and compare-and-append at the log itself (holds). The build fails when any verdict moves, so a change that weakens a rule is caught by the model before a cluster ever sees it.

The model is explicit about its edges: one object at a time, a projection that is the last record folded, time as the heartbeat tick, no liveness. Each is stated beside the specification.

1.3 The specification, in its own words

The whole model is under two hundred lines, and the parts that matter are short enough to read here. The invariant is one line. An engine is current when it is alive, its membership view is the store's latest, and it has read the log to the end; two current engines must hold the same last record for every object:

Current(e) == alive[e] /\ view[e] = KV /\ cursor[e] = Len(log)

Agreement ==
  \A e, f \in Engines :
    (Current(e) /\ Current(f)) => \A o \in Objects : proj[e][o] = proj[f][o]

A write is what an engine does for an object its view says it owns. The two lines that begin with a knob are the fences the checker asked for. WriteFenced is the rule the code runs today: refuse to write an object whose log epoch has already outrun this view. AppendFenced is the stronger alternative that was checked and not needed:

Write(e, o) ==
  /\ alive[e] /\ Owns(e, o)
  /\ Len(log) < MaxLog
  /\ AppendFenced => view[e].epoch = kvEpoch
  /\ WriteFenced => seenEpoch[e][o] <= view[e].epoch
  /\ LET r == [obj |-> o, by |-> e, epoch |-> view[e].epoch] IN
       /\ log' = Append(log, r)
       /\ proj' = [proj EXCEPT ![e][o] = r]
       /\ seenEpoch' = [seenEpoch EXCEPT ![e][o] = r.epoch]

Each configuration is a handful of constants. The first line declares the verdict the checker must reach, and the build compares. This is the one that describes the code as it ships, and it is required to hold:

\* expect: holds
CONSTANTS
  Engines = {1, 2}
  Objects = {1}
  MaxEpoch = 6
  MaxLog = 4
  Missed = 3
  ReplayFenced = TRUE
  SkipMode = "self"
  WriteFenced = TRUE
  AppendFenced = FALSE
INVARIANTS TypeOK OneWriterPerEpoch Agreement

The configuration that describes the rules as first shipped differs in three constants, ReplayFenced = FALSE, SkipMode = "owned" and WriteFenced = FALSE, and its first line reads expect: violated. That file is kept on purpose: a run that stops finding the counterexample is a change in the model, not a fix in the code.

1.4 The counterexample, step by step

This is the checker's own trace against the rules as first shipped, two engines and one object, with the state written out in words. The checker's trace has seven transitions; the one left out here is a heartbeat tick that only bumps the store's revision. No partition, no crash, nothing unusual:

Under the rules the code runs now, step 4 folds the record, because the tail skips only what this engine wrote itself, and the trace cannot be completed. The checker confirms that by exhausting every other ordering too.

2. The core is tested by generation

The state machine, replay and the projections are pure functions, so they are run over thousands of generated inputs against invariants rather than a handful of hand-written cases. Every property below is a test that draws random sequences on each run and, on a failure, shrinks it to the smallest input that reproduces it.

State transitions, over random result sequences:

• Problem-class notifications are emitted only from hard states, and never while flapping.
• A recovery is notified only from a hard problem.
• The flap value stays within zero and one, and stable input always converges out of flapping.
• The attempt counter stays within zero and max attempts.
• Every transition schedules exactly one next check: a retry while soft, a regular check otherwise.
• Replaying a result sequence is deterministic.

Replay, over random logs of state changes and check results:

• Each object's replayed state is the last state change for it, in log order, and its last-seen time is the last check result for it.
• A host is marked down in the reachability graph exactly when its last state change was a hard problem.
• Restoring from a snapshot at any point and folding the rest equals replaying from the start, reachability included.
• Replaying the same log twice yields equal results.

Each of those is checked against a reference model written independently, a plain last-write-wins fold, never against a copy of the implementation.

Elsewhere:

• The projection: folding any generated sequence of state, ack and downtime events reproduces an independent reference's state, last-seen and suppression tables.
• Ownership: the owner of an object is deterministic and independent of the order members are listed in.
• Business processes: and, or and quorum are invariant under permutation of their children, evaluation is deterministic, and an and never ranks below a child while an or never ranks above one.
• Notifications: a notification stays open exactly while some contact has neither a delivery nor a terminal failure, and no request is delivered under an ownership view older than the one it was stamped with.
• Label selection: an indexed select returns exactly what a full scan over every object returns.
• Object identity round-trips through its text form, including the pre-existing prefixless host form.

3. What is proven against a real process

Replay is also checked the unsubtle way: an engine is started, sent kill -9 in the middle of a check, restarted, and compared. The projection it rebuilds is identical, history included. See Event sourcing.

The Livestatus status table is pinned against a replay of real Thruk traffic. And the checks that gate the repository are themselves tested, one case per defect that once shipped, so a green that measures nothing is caught the same way as a red.

Nothing on this page is a claim about a test that was run once. Every check here runs on every change, and the build fails when any of them does.