Keep a checked specification connected to the shipped service

The intended conformance statement is that every implementation behavior allowed by the declared environment maps to a behavior permitted by the specification. The environment includes failure modes, storage guarantees, clocks, message behavior, and caller obligations. The mapping defines which implementation events and states represent abstract actions and observations. A proof about a protocol library may leave serialization, resource exhaustion, system calls, and deployment orchestration outside its verified boundary. State those boundaries explicitly rather than implying that correctness of one layer covers all code that happens to call it.

Full implementation verification can connect program-level reasoning to state-machine refinement, as projects such as IronFleet demonstrate under their stated methodology and assumptions. Other teams use a design model plus disciplined reviews, model-based tests, deterministic simulation, and runtime trace checks. Those methods can expose important defects without constituting the same universal proof. Match the language of the claim to the evidence obtained. A useful partial claim identifies its remaining correspondence obligations instead of treating every unverified layer as either irrelevant or a reason to abandon specification work.

A trace checker can map a captured execution to the model and reject an impossible transition or an inconsistent history. Its instrumentation must observe the relevant boundaries, preserve identities and ordering, and classify missing events honestly. A dropped trace segment can make an actual violation invisible or create a spurious apparent violation. Test the checker and instrumentation with known legal traces and deliberately invalid mutations. A passing checker over an incomplete observation is evidence only for the property and information it actually examined.

Finite test campaigns explore a selected subset of schedules and configurations. Record planned cells, executed cells, failures, inconclusive outcomes, and the coverage criterion rather than converting the passing fraction into a production reliability probability. Repeated identical schedules can produce many passing operations while adding little new behavioral coverage. A simulation's deterministic replay is valuable for diagnosis, but its network, storage, and timing abstractions still need validation against the real service. A test harness and a specification can also share the same mistaken assumption, so independent semantic review remains necessary.

Retain the specification revision, checked properties, parameter domains, fairness assumptions, tool versions, solver status, implementation revision, configuration, and mapping used for each release claim. Link counterexamples to regression tests and document which code boundary enforces each modeled atomic action. When a storage engine, retry policy, deduplication horizon, scheduler, or wire format changes, review the affected assumption and correspondence obligations. A comment stating that a model exists is not evidence that the new mechanism still implements it. Include operational checks for assumptions that can become false after deployment.

The quadratic instrument illustrates the limits of a single passing example. Reset, set a=1 and x=0, predict y=0, then Play or Step. Separately Reset, set a=2 and x=0, predict y=0 again, then Play or Step. Both selected functions agree at zero; at x=1 they produce one and two. The instrument computes its declared family exactly and is not comparing service implementations. Its narrow lesson is that agreement on an observed input does not establish agreement everywhere, just as finite conformance observations do not establish universal behavior inclusion.