Learn · All the Ways It Can Break

growing

Choose the Question Before the Notation

A model earns every included detail by the observation it must explain.

formal-methods, modeling, abstraction, specification, learn

This is the first of thirty-two chapters. You will turn a vague wish—“verify the job service”—into one checkable question, choose the observation that would answer it, and write a refusal boundary. You will also learn why implementation fidelity and modeling rigor are different virtues. No formal notation is needed yet; later tools will consume the model card built here.

A map is useful because it leaves things out

A subway map preserves stations, lines, transfers, and order. It usually discards the exact curve of the track, the buildings overhead, and the distance between adjacent stops. That would be negligence in a construction drawing. It is clarity in a route map.

Abstraction — a representation that preserves selected observations while discarding distinctions irrelevant to them. Leslie Lamport's high-level view of TLA+ explains why a specification describes behavior above code-level detail.

The same rule applies to software. “Verify this service” is not one question. It might mean:

can a canceled job publish a result?
can two users obtain the same private result?
can capacity fall below zero?
does every accepted job eventually finish?
can a retry execute the same irreversible effect twice?

Each question needs a different observation. A publication-safety model must observe whether publication occurred and which job generation authorized it. A capacity model must observe credits acquired and released. A liveness model must observe an entire behavior over time. Combining everything immediately does not create a stronger model. It creates more states before the claims have even been separated.

Prediction — choose the smallest model that can answer the stated question.

Write the model card

Before a language, write five lines:

Field	Job-service model
Purpose	Decide whether cancellation can be followed by publication.
Included state	Job identity, lifecycle phase, canceled flag, published flag.
Actions	Accept, start, cancel, complete, publish.
Observation	Whether a published job had already been canceled.
Refusal boundary	Payload computation, storage layout, timing, authentication, and recovery after process loss.

The final row is as important as the first. A refusal boundary says which conclusion the model cannot support. It prevents a later green result from quietly expanding into “the service is correct.”

The card can expose a defect before any checker runs. If the question asks whether an old attempt can publish after a retry, the state needs an attempt or generation identity. A model with only running and canceled cannot distinguish the old attempt from the new one. The missing state is visible because the purpose came first.

Rigor is not resemblance to the implementation; rigor is preserving every distinction needed by the claim and naming every distinction deliberately left outside it.

Under the hood: observations define adequacy

Imagine two concrete situations that the model maps to the same abstract state. That merge is sound for this purpose only if every admitted future action produces the same relevant observations from both situations. If one can later publish and the other cannot, the abstraction erased a distinction the question needs.

This gives an experienced engineer a practical review test. Do not ask whether the model contains every production field. Pick two production states that the model merges and try to construct a future that makes the claimed observation differ. One such future is a counterexample to the abstraction.

The opposite failure matters too. Distinguishing two payload encodings that cannot affect cancellation or publication multiplies states without increasing the model's power to answer its question. The checker pays for that detail; the claim receives nothing.

Refuse before extending

When a reviewer asks, “But what about authentication?”, the disciplined answer is not “the model probably covers it.” It is one of:

Authentication cannot change the current observation, so it remains outside.
Authentication can change the observation, so the current claim is too broad.
Authentication is a separate relational question and deserves a separate model.

That answer keeps growth deliberate. Later chapters will use different tools for behavior, relationships, code values, and thread schedules. The separation starts here, before tool preference can choose the question on the reader's behalf.

Lessons

“Verify the system” must be divided into questions with observable answers.
A useful abstraction preserves distinctions that can change the selected observation.
Extra implementation detail can enlarge the state space without strengthening the claim.
A refusal boundary prevents a scoped result from becoming a general assurance claim.
The five-line model card comes before language, syntax, or checker selection.

Practice

Retrieval. Without looking back, write the five fields of the model card.
Discrimination. A payment model records amount, currency, request identity, and status but omits the CSS class of the submit button. Is that omission an abstraction or an error for the claim “one request causes at most one debit”?
Transfer. Write a purpose, observation, and refusal boundary for the question “Can a document remain visible after its access grant is revoked?”

Worked answers

Purpose, included state, actions, observation, and refusal boundary.
It is an abstraction: the CSS class cannot change debit identity under the stated claim. If UI state can issue an additional request, model that request action rather than its styling.
One adequate answer: purpose—find a read after revocation; observation—the principal and document returned by each read; included state—grant identity, revocation state, cached copies, and read actions; refusal—document contents, typography, and unrelated grants. A cache may force the model to include more state if it can serve after revocation.

References

Leslie Lamport. “A High-Level View of TLA+.” 2021. — behavioral specifications above implementation detail and the role of state and actions
Daniel Jackson. “Software Abstractions: Logic, Language, and Analysis.” MIT Press, 2012. — purpose-driven lightweight modeling and analysis

Keep Only Differences That Change the Future →

Suppose a service accepts a job, starts it, and eventually publishes a result. One team draws the database schema. Another draws the network. A third writes the class hierarchy. All three artifacts may be accurate, yet none answers the question that woke the engineer at 2 a.m.: can a canceled job publish? A formal model begins by making that question smaller and sharper. The first model may ignore payload bytes, database indexes, hostnames, retry delays, and the color of the button. It keeps job identity, lifecycle phase, cancellation, and publication because those distinctions can change the answer. The omitted details are not forgotten; they are refused explicitly. This is the first discipline of formal work. Choose the observation before the notation. A model is not a miniature implementation. It is an instrument built to distinguish the futures relevant to one claim. More detail can make that instrument slower and less truthful when the detail hides the missing distinction that actually decides the question.