Adversarial traces: check every partial execution

Record each node's role, current term, durable vote, durable log, known commit index, applied index, and active configuration. Record messages as separate objects with sender, receiver, term, request context, and payload. Delivering, duplicating, delaying, or dropping a message changes a specific transition; a timeout merely introduces another eligible event. This explicit representation stops the test author from silently granting a vote, changing an entry, or removing a member to make a desired narrative work.

A partition can leave an old leader believing it still leads while a majority elects a higher-term leader. The minority's uncommitted suffix may be replaced when communication resumes. Its already committed prefix must not be contradicted, and it must not serve unsupported linearizable reads while isolated. Track client invocation and response events too: a lost response can leave the client uncertain even after a command is committed. A test that only compares final database contents can miss both a stale read and an earlier invalid acknowledgement.

Insert crash points before a required storage operation, after issuing it, after its durability completion, before sending the dependent reply, and after that reply is delivered. Recovery must use only the state the storage model says survived. Replaying all issued writes as if they were durable erases exactly the failures the test should investigate. Include old messages after restart, duplicate append requests, stale vote responses, and snapshots with different boundaries. The oracle must reject an impossible recovered state rather than quietly normalize it.

For membership tests, preserve the actual configuration activation rules and quorum predicates. A test harness that always uses the newest desired membership can accidentally make an unsafe implementation look correct. Likewise, an authority check mocked as an unconditional success removes stale-leader read failures. Keep deterministic seeds and a replay log, then minimize failing traces while preserving their invariant violation. A shorter counterexample is usually easier to turn into a precise regression and a corrected safety argument.

A bounded model checker can exhaust its stated state space and establish that its modeled oracle has no counterexample within those bounds. It does not automatically cover more nodes, longer logs, unmodeled disk behavior, or integration code. Fairness and eventual-timing assumptions are needed when asking liveness questions; a test that drops every message forever cannot reasonably require every client request to finish. Conversely, allowing a system to stop indefinitely is not evidence that its progress mechanism meets an operational target.

The probability lab illustrates a separate, deliberately assumed sampling claim. Reset, explicitly set success probability to 0.10 and trials to ten, interpret success as observing a failure, predict the zero-success bar, then Play or Step. For another comparison Reset and explicitly set probability 0.10 and trials twenty. The exact binomial model assumes independent trials with a known common observation probability. Real test schedules can be correlated and their failure probability unknown, so these bars neither enumerate executions nor certify a passing consensus implementation.