Wins

Recovery snapshots race in-flight replication: recovered coordinator misses acked writes

Handoff · caught by CoordinatorHoldsAcked · fixed in gen 1 · 2026-07-24 14:58:05 UTC

The system is a memory-only replicated KV store on a substrate that evicts processes arbitrarily: three replicas hold all state in RAM, a fixed coordinator quorum-commits writes (apply locally + one peer holds it), and an evicted replica recovers by merging point-in-time snapshots from every other replica before serving. The design assumed that merging snapshots from ALL peers guarantees a recovered coordinator holds every acked write that still survives, stated as the invariant CoordinatorHoldsAcked. TLC refuted it with a 13-step counterexample: a write is committed and acked while its replication push to peer r2 is still in flight (held by coordinator + peer r1). The coordinator is evicted and begins recovery; it snapshots r2 BEFORE the in-flight push lands there, then r1 (the only holder) is evicted, then the coordinator snapshots the now-empty r1. Every peer was consulted, yet the acked write dodged both snapshots and survives only at r2, where the late push finally landed. The coordinator finishes recovery and serves without an acked write that is still alive in the system. The refutation generalizes: snapshots are point-in-time and deliveries can be delayed arbitrarily, so no finite number of collect rounds closes the window. The corrected design demotes coordinator completeness from a safety property to an eventual one (anti-entropy gossip restores the write to the coordinator), documents a read-your-writes gap across coordinator failovers (even 2-of-3 quorum reads can miss a write degraded to one surviving copy), and checks the weakened safety invariant CoordinatorHoldsOwnCommits: a ready coordinator always holds every non-doomed write acked in its own incarnation. The fixed spec passes with the full state space exhausted (95,028 distinct states), alongside the loss-model invariant that an acked write is only ever lost when eviction destroys its last copy.

Missing transaction-ID validation: a stale response would be silently adopted by the next command

webmtp · caught by RespTidMatchesOutstanding · fixed in gen 2 · 2026-07-23 15:49:36 UTC

The system is a browser-side initiator speaking an MTP/PTP-style transport to a USB responder: Command → optional Data → Response containers over FIFO bulk pipes, each container carrying a transaction ID, one outstanding transaction at a time. The bug was found through the spec rather than a violation trace. Modeling the receive path forced a decision the implementation had skipped: the model's response-accept action naturally required the inbound container's transaction ID to equal the outstanding command's (invariant RespTidMatchesOutstanding), but the implementation accepted any RESPONSE-type container without comparing IDs. The check proved the unchecked code is sound against a conforming responder — under FIFO delivery and the one-outstanding discipline, IDs cannot mismatch — which is precisely why testing would never catch it. The soundness argument, however, assumes a clean pipe, and the initiator's environment breaks that assumption routinely: it can be killed and restarted mid-transaction (a page reload), abandoning a command and leaving its response in the inbound pipe. On reconnect, the next command would silently adopt the previous command's response — for example, treating leftover read data as the status of a delete. A wrong answer with no error. The fix: the initiator validates the response's transaction ID and treats a mismatch as a transport failure. The corrected design is in the current generation: a reject-on-mismatch action models the failure path, and NoTransportFailure proves that path unreachable against a conforming responder — the defensive check can only ever fire on genuine desynchronization, never on the happy path. The spec later grew bidirectional data phases and an object-info/data pairing rule (DataDirectionOK, SendObjectPaired) with all invariants still holding.