Learn · All the Ways It Can Break
growing
Green Has a Boundary
Every checker result keeps its encoded claim, assumptions, finite scope, and unsupported behavior attached.
You will distinguish exhaustive finite exploration, bounded search, and an inductive proof obligation; detect two forms of vacuity; and write an honest result sentence. This chapter completes the conceptual foundation. The next chapter begins the first public language with TLA+ values.
Four greens that are not interchangeable
Consider the property “no canceled attempt publishes.” Four reports might say:
| Result | What it may establish |
|---|---|
| finite explicit exploration completed | no reachable state in that concrete finite model violates the invariant |
| bounded symbolic search through length 10 completed | no admitted trace of at most ten steps violates the property |
| inductive obligations completed | the candidate invariant initializes, survives each admitted step, and implies the safety property |
| schedule exploration completed under a bound | no instrumented schedule within the declared exploration violates the assertion |
The rows are not levels on one confidence meter. They quantify over different objects. Later chapters will make each precise in its native tool.
Vacuity — a property passes for a reason that does not exercise its intended condition, often because the antecedent or relevant behavior is unreachable. The Alloy tutorial and model-checking literature use explicit instances and reachability checks to expose this class of mistake.
Vacuity has more than one costume
The simplest form is an implication whose antecedent never holds:
if published then not canceled
If published is always false, the property passes. A second form is an overconstrained model. A state constraint, fact, assumption, or precondition may remove the failing action. The checker correctly checks the smaller world; the report incorrectly speaks about the larger one.
Two witnesses resist this failure:
- a positive witness reaches the useful behavior the property regulates;
- a negative control introduces one known defect and makes the check fail.
Neither witness proves the model complete. Together they show that the property is not green merely because its subject is absent and that the tool can expose the defect shape the chapter claims it checks.
Bounds precede the claim
Finite tools need finite work. Bounds may limit jobs, principals, messages, trace length, loop iterations, threads, branches, or preemptions. Bounds are not embarrassing implementation details. They define the quantified domain.
“No violation found for two jobs and traces through eight actions” is useful when the smallest expected defect fits that scope. It is not equivalent to “no job count and no longer trace can violate the property.” A small-scope argument can justify why the selected bound is likely to expose a structural mistake, but only a proof or a separately established cutoff can remove the bound from the conclusion.
Resource exhaustion is also a result, not a green check. If the tool stops before completing its declared search, the honest status is incomplete, exhausted, or unknown according to the tool—not “no counterexample found” with the stopping condition omitted.
The smallest honest verification report is a claim plus its model, assumptions, bounds, completion status, witnesses, and residual risk.
Write the sentence another engineer can audit
Use this template:
Tool and version checked PROPERTY over MODEL.
Under ASSUMPTIONS and BOUNDS, the declared search COMPLETED/STOPPED.
It found RESULT.
Positive witness W and negative control N exercised the boundary.
The result does not establish REFUSAL; residual risks are R.
For example:
The checker exhausted the reachable graph for two jobs, one credit, and the
five declared actions. No reachable state published a canceled attempt. A
successful-publication witness was reachable, and removing the cancellation
guard produced the expected four-action trace. The result does not establish
the production implementation, larger job domains, liveness, or behavior of
failures absent from the model.
This is longer than “verified.” It is also the minimum from which a reviewer can decide whether the result matters.
Under the hood: quantifiers are the real output
Every method chooses a quantified set:
- all states reachable in one finite graph;
- all traces no longer than a bound;
- all values admitted by a proof harness and its assumptions;
- all schedules visible through instrumented primitives and configured limits.
The tool's algorithm determines how it searches or proves over that set. The model and configuration determine what belongs to the set. Result interpretation fails when the prose silently replaces the actual set with “everything the system could ever do.”
Experienced engineers should ask for the quantifier before the verdict: all what, under which semantics, until which completion condition? That question works across every tool in this book.
Lessons
- Different tools and modes produce green results over different quantified domains.
- Vacuity can come from an unreachable antecedent or an overconstrained model.
- Positive witnesses and deliberate negative controls make a property's reach observable.
- Bounds and resource exhaustion belong in the result, not in a footnote.
- An auditable report states claim, model, assumptions, bounds, completion, witnesses, and residual risk.
Practice
- Retrieval. List the seven parts of the result envelope without looking back.
- Discrimination. Explain why “all traces through length ten” and “all states in a completed finite graph” are not interchangeable even if both checks are green.
- Transfer. Rewrite “we formally verified the retry logic” as an honest hypothetical result using named bounds and one forbidden inference.
Worked answers
- Claim, model/tool identity, assumptions, bounds, completion status, witnesses or controls, and residual risk.
- A longer path may revisit finite states already exhausted by the graph search, while a length-bounded search stops by trace length and may not cover states requiring more steps. Their quantified sets and completion meanings differ.
- Example: “Tool X exhausted the model with two requests, one server, loss and duplicate delivery, and at most one retry; no request identity produced two effects. A mutation that removed deduplication failed. This does not prove the production storage transaction, more retries, crashes, or liveness.”
References
- Leslie Lamport. “Specifying Systems.” Addison-Wesley, 2002. — finite models, invariants, temporal properties, fairness, and result interpretation
- Apalache Project. “Principles of Symbolic Model Checking with Apalache.” — typed symbolic transitions, bounded checks, and invariant modes
- Alloy Project. “Alloy Tutorial.” — scopes, instances, assertions, and Analyzer interpretation
- Kani Project. “The Kani Rust Verifier.” — proof harness outcomes, supported behavior, and limitations
- Loom Project. “Loom crate documentation.” — instrumented exploration, bounds, and limitations