Build a ledger, not a verdict pile

Use one row per claim:

Do not write “formal verification: passed.” A reviewer should be able to remove one row without changing the meaning of the others.

The missing edge is usually correspondence

A model can be internally correct and irrelevant to the program. Strengthen the edge with independently checkable artifacts:

• generate shared constants or schemas rather than retyping them;
• replay model counterexample events through an implementation harness;
• compare a small executable model and production transition function on the same cases;
• trace each fault-model action to a real adapter or documented exclusion; and
• run the exact production feature flags, target widths, and dependency versions named by code-level claims.

None of these automatically proves full refinement. They turn an assumed link into narrower evidence and make drift observable.

Do not add unlike greens

Three bounded checks do not yield “three times the confidence.” They may share the same wrong abstraction, omit the same fault, or all depend on one mistranslated constant. Evidence is often correlated. Combine it as a structured argument:

C1 follows from model M under assumptions A within bound B.
Fixture F shows implementation event E maps to model action X.
Negative control N demonstrates that M and its checker reject the known defect D.
Risk R remains because fault Y and populations beyond B are not covered.

Capstone: one-use credential redemption

Build a service that issues a credential for one protected resource. The credential may be redeemed once before expiration. Two gateways can receive the same credential concurrently. Gateways send redemption requests to a replicated authority over a network that can delay, duplicate, and drop messages. Each gateway also deduplicates local retries. A Rust decoder reads a version, expiry tick, resource identifier, and credential identifier from a bounded byte record.

Do not begin by choosing every tool. Write claims first:

1. Structure. An issued credential relates exactly one principal to one resource; revoked credentials authorize none.
2. Behavioral safety. At most one redemption becomes committed, and expiry or revocation is never followed by a successful commit.
3. Behavioral progress. Under named delivery and scheduling assumptions, an eligible retried redemption eventually receives a terminal answer.
4. Executable fault behavior. Duplicate, reordered, lost, and timed-out messages preserve the safety claim.
5. Code safety. Every accepted record is decoded without overflow or out-of-bounds access and preserves all fields.
6. Local concurrency. Two instrumented threads cannot both mark the same local credential newly redeemed.

Choose the smallest portfolio. A defensible default is Alloy for Claim 1; TLA+ with TLC for Claims 2 and 3; Stateright for Claim 4 if the executable actor and fault vocabulary materially improves correspondence; Kani for Claim 5; and Loom for Claim 6. Apalache is useful only if a bounded symbolic or induction obligation adds evidence the TLC route does not already supply. Omitting an unneeded tool is a correct decision.

Completion rubric

The capstone is complete when another engineer can inspect:

• a claim ledger with no “the system is correct” row;
• one failing negative control and checked repair for every selected lane;
• one positive witness preventing deny-all or unreachable behavior;
• minimized counterexamples explained as domain actions;
• exact scopes, constants, trace lengths, unwind values, schedule limits, tool versions, and feature flags;
• at least one model-to-implementation correspondence artifact per code-relevant claim;
• one credible tool refusal per claim;
• a residual-risk list that includes omitted faults and semantic limitations; and
• a clean-room rerun from public setup instructions.

The rubric does not award points for line count, number of tools, solver time, or a green dashboard. It rewards evidence that could falsify the claim and a conclusion no broader than that evidence.

A result sentence template

Use this without flattening the details:

For claim C, tool T found [no witness / witness W] in artifact M under assumptions A and bounds B.
Negative control N [failed as expected / did not, invalidating the run].
Correspondence evidence E links M to implementation surface I.
This does not cover X; residual risks are R.

If the sentence feels long, the claim may still be compound. Split it before shortening the evidence.

Lessons

• Evidence composes by claim links, not by counting green tools.
• Model correctness and model-to-code correspondence are separate obligations.
• Negative and positive controls test whether evidence is connected to its subject.
• Bounds, versions, and feature flags are part of the result.
• Shared abstractions create correlated failure risk across tools.
• Residual risk is an output of the work, not an embarrassment to hide.
• Refusing an unnecessary tool improves the portfolio.

Practice

1. Retrieval. Name the five columns of the claim ledger.
2. Discrimination. Why does replaying a model trace through code strengthen but not necessarily prove refinement?
3. Transfer. Complete the credential capstone, then remove one tool without losing a claim—or explain precisely why none can be removed.

References

1. Leslie Lamport. Auxiliary Variables in TLA+. — relating behaviors through added or hidden state
2. Daniel Jackson. Software Abstractions. — small models, counterexamples, and abstraction
3. John Rushby. The Interpretation and Evaluation of Assurance Cases. — structured claims, evidence, and defeaters