> Section: [11. Project](https://jaque.sh/docs/project/status.md)
> Next: project/roadmap
> Index: https://jaque.sh/llms.txt


Most of jaque's guarantees are stated as invariants and checked
mechanically, not asserted in prose. [Status](https://jaque.sh/docs/project/status.md) 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](https://jaque.sh/docs/deployment/cluster-and-coordination.md)
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:

```tla
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:

```tla
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:

```tla
\* 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:

| Step | Action | What is true afterwards |
|---|---|---|
| 1 | Engine 2 writes the object under epoch 1 | The log holds one record, written by engine 2. Engine 2 folded it; engine 1 has not read it yet. |
| 2 | Engine 2 leaves cleanly | Engine 1 is the only member. |
| 3 | Engine 1 refreshes its view | Engine 1 now owns the object. Its tail is still at position 0. |
| 4 | Engine 1 reads the record | It skips it: the object is "owned", and owned records were treated as the engine's own. Engine 1 still holds no state for the object. |
| 5 | Engine 2 restarts | It replays the log and holds the record again. |
| 6 | Both refresh to the same view | Both are current. Engine 2 holds the record, engine 1 holds nothing. `Agreement` is violated. |

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](https://jaque.sh/docs/concepts/event-sourcing.md).

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.