The moment after which repair is too late

Take the intended rule:

A canceled attempt must not publish.

A violating trace may be only four actions long:

Accept(7) → Start(7) → Cancel(7) → Publish(7)

After the fourth action, the property is false for that behavior. A fifth action can remove the result from storage, but it cannot change the earlier publication event. The four-action prefix is enough evidence.

Turn prose into a predicate

Suppose model state records phase, activeAttempt, and publishedAttempt. One invariant says:

if publishedAttempt is present,
then it equals activeAttempt
and phase is not canceled

The words come before notation. If $P(s)$ is the predicate above, the invariant claim is that every reachable state $s$ satisfies it:

$$\forall s \in \operatorname{Reachable}: P(s).$$

This compression exposes two obligations that prose can hide. First, what counts as reachable depends on the initial predicate and transition relation. Second, the state must remember enough to evaluate $P$. If publication is only an event and leaves no trace in state, a state invariant cannot mention that it happened. The model can retain a publication flag, or the later language can state a property over behaviors.

A type invariant answers a different question. It might say that phase is one of idle, running, canceled, or completed and that credit is 0 or

1. Type correctness can pass while publication safety fails. Keeping both

claims separate makes the counterexample informative.

A checker needs a reachable failure

Writing the invariant is not enough. A model can make it pass by preventing every job from starting. The safe state then exists because useful behavior does not.

Pair the invariant with a positive reachability witness:

Some behavior accepts, starts, completes, and publishes one job.

Then add a negative control: deliberately weaken the cancellation guard and confirm that the checker reaches Cancel(7) → Publish(7). A checker that stays green under the known defect has not exercised the intended claim.

Under the hood: why finite prefixes matter

An execution may continue forever, so a checker cannot generally wait for its end. Safety has a special shape: if a behavior violates the property, some finite beginning of that behavior cannot be extended into any satisfying behavior. The failure is already complete.

This does not mean every safety check is computationally easy. The state space may be enormous or infinite. It means the evidence shape is finite. Explicit and symbolic checkers exploit that shape differently; both can return a finite counterexample when they find one.

The next chapter meets the complementary difficulty. No finite prefix proves that a job will never finish, because the next action might finish it. A progress failure concerns the infinite continuation and the promises made about which enabled actions the environment will eventually choose.

Lessons

• A safety violation has a finite bad prefix that no continuation can repair.
• An invariant is a state predicate required of every reachable state.
• Type invariants and domain safety invariants answer different questions.
• The state must retain enough information to evaluate the property.
• Positive witnesses and deliberate negative controls detect vacuous checks.

Practice

1. Retrieval. Define a finite bad prefix without using the word “error.”
2. Discrimination. Is “every queued item is eventually processed” a state invariant? Explain what a finite trace can and cannot show.
3. Transfer. For a one-use password-reset link, write one safety invariant and the shortest action trace that would refute it.

References

1. Bowen Alpern and Fred B. Schneider. “Defining Liveness.” Information Processing Letters, 1985. — formal safety/liveness decomposition and finite-prefix characterization
2. Leslie Lamport. “Specifying Systems.” Addison-Wesley, 2002. — invariants, behaviors, and model checking in TLA+