Turn an abstract failure trace into a controlled fault schedule

Find the first state that violates the checked property, then trace which earlier actions made that state possible. Preserve relevant identifiers, durable writes, ownership epochs, message dependencies, and failure assumptions. Remove irrelevant work only when the smaller trace still exhibits the same violation. Record both the original witness and the reduced schedule so reviewers can see which facts were retained and which were merely incidental search choices.

Separate abstract events from implementation hooks. An action called Commit might correspond to a database transaction, a receiver's durable acknowledgement, or several local operations depending on the model. Establish which concrete event witnesses completion of the promised effect. Logging that a function started is not proof that its durable effect completed. Likewise a client timeout does not prove absence of that effect. An independent oracle should inspect the state whose contract is being tested, rather than relying only on the worker's own success counter or the same log record whose loss is under investigation.

Suppose a worker commits an external effect and only later records that request r is complete. If the two facts are not atomically coupled or protected by receiver-side idempotency, a crash between them can leave the effect durable but the retry guard absent. Introduce a test barrier after the effect's verified commit and before the deduplication record's commit, terminate the worker, restore it from the allowed persisted state, and retry the same identifier. Verify both the execution trace and the external effect count. A process kill tests different assumptions from a storage-loss event or a network partition.

A model may intentionally overapproximate failures. If the implementation commits the effect and deduplication fact in one actual atomic consistency domain, the proposed intermediate state may be impossible. In that case, supply evidence for the atomic boundary and refine the model instead of forcing an impossible injection. When effects cross independent systems, a local transaction alone may not couple them; a receiver's stable idempotency contract or another explicit protocol can change the analysis. A compensation action has its own failure and observability semantics and does not automatically restore an at-most-once effect property.

If the implementation reproduces the violation, keep a regression that asserts the independent contract outcome under the controlled schedule. A fix must close the mechanism and survive the same restart or retry semantics, not merely alter a log message or make the race less likely. If the test does not reproduce the abstract witness, determine whether the hook missed the intended boundary, the oracle was incomplete, or an implementation guarantee excluded the behavior. Absence in a few random runs is not a proof of impossibility. Deterministic simulation can explore many controlled schedules while retaining its own environment-model limits.

The reliability instrument shows an availability fact that cannot settle this effect-safety question. Reset, set n=3 and k=1, predict two available replicas and majority threshold two, then Play or Step. Separately Reset, set n=3 and k=0, predict three available and threshold two, then Play or Step. Both settings have a majority, but the model contains no effect commit, deduplication record, or crash-recovery protocol. A reachable majority does not rule out duplicate effects at another boundary; use the counterexample's actual state and oracle to test that property.