Learn · All the Ways It Can Break

growing

Strengthen What Must Survive One Step

An inductive invariant begins true, survives an arbitrary admitted step, and implies the safety claim.

formal-methods, apalache, inductive-invariant, proof, learn

You will formulate the three induction obligations, run a one-step preservation negative control and repair, and recognize when a true safety property needs a stronger candidate invariant. Experienced readers can treat the candidate as an inductive strengthening rather than a test oracle.

Start from every candidate state

The specimen defines the induction premise explicitly:

tla code/all-the-ways-it-can-break/symbolic-capacity/Capacity.tla#induction-premise Capacity.tla This is broader than Init: it includes every state the candidate claims is safe.

Run one symbolic step from that premise with NextBug and NextFixed. The broken action finds used = 2 followed by used' = 3. The guarded action has no such successor. This establishes a preservation result for the encoded candidate and transition relation.

Proof structure — identify what a preservation check cannot establish alone.

The three obligations

For candidate Ind and desired property Safe:

Init => Ind
Ind /\ Next => Ind'
Ind => Safe

If all three hold, ordinary induction gives Safe for every reachable state. If preservation fails in an unreachable state, strengthen Ind with the missing fact that excludes it—provided that fact itself initializes and is preserved. Do not add Safe as an assumption to make the obligation circular.

What the tool did and did not do

The paired one-step checks mechanize preservation for the supported typed fragment. The bounded checks from Chapter 16 remain useful negative controls. The conclusion still concerns the model, not an implementation, and it retains every assumption in Init, NextFixed, the type annotations, and the solver translation.

Lessons

Induction quantifies over arbitrary candidate states, not only reached prefixes.
Initiation, preservation, and implication are distinct obligations.
A non-inductive safety property may need truthful auxiliary facts.
Strengthening excludes impossible premises; it must not assume the conclusion.
Bounded witnesses and induction obligations complement rather than replace each other.

Practice

Retrieval. Write the three obligations from memory.
Discrimination. A candidate excludes used = 2 solely to avoid the broken acquire step, but Init and Next can reach two. Is it a valid strengthening?
Transfer. Propose an inductive candidate for a token bucket that preserves both nonnegative tokens and an upper capacity.

Worked answers

Init => Ind; Ind /\ Next => Ind'; Ind => Safe.
No. Preservation may pass, but reachable state two violates the candidate.
Include both 0 < tokens= and tokens < Capacity=, then guard consumption and refill so each boundary survives one step.

References

Apalache team. Inductive invariants. — initiation, transitions, and invariant checking
Leslie Lamport. Specifying Systems, Chapter 5. — invariance proofs and strengthening

← Ask for the Whole Bounded Trace Everything Begins as a Relation →

Checking longer prefixes always begins at Init. Induction asks a different question: suppose an arbitrary state satisfies the candidate invariant. Must every admitted next state satisfy it too? The capacity specimen makes every value from zero through two a possible premise. The broken acquire action fails immediately from two; the guarded action preserves the range. Preservation alone is not a proof. The candidate must also hold initially and must imply the safety property. These three obligations—initiation, preservation, implication—are kept separate so a one-step green result cannot masquerade as an unbounded theorem.