4.3 Validating Change

Every engineering process eventually asks the same question: what evidence is sufficient to accept this change? Code review, testing, static analysis, operational measurement, and expert judgment answered that question long before coding agents arrived. Commodity implementation does not make those techniques obsolete. It makes them more important, because changes can now arrive faster than human inspection can scale.

Validation begins with an obligation. If the obligation is settled, evidence can test whether the change satisfies it. If the obligation is still a hypothesis — whether users want the feature, which workflow they prefer, which tradeoff is acceptable — no test suite can manufacture the missing product knowledge. In that regime the evidence is experimental. MAGE can govern the experiment and preserve known constraints; it cannot turn an open question into a mechanical truth.

4.3.1 Independent Evidence

To validate a change is to assemble evidence that bears on its obligations and decide what consequence that evidence should have. The producer's own report is rarely enough. A human says the change is correct; an agent says the tests pass; a tool announces completion. Each claim may be useful, but the strongest assurance comes from evidence generated independently of the judgment seeking admission.

For consequential changes, prefer evidence that can challenge the producer's own claim rather than relying on self-report alone. Where the consequence warrants it, place admission authority outside the producer's ability to redefine success.

That evidence can come from several sources. A model may expose a system-level invariant. A test may exercise a behavior. A compiler or type system may reject an illegal state. A reference implementation may supply a differential oracle. A metric may reveal degradation. A human reviewer may decide a property that remains judgment-laden. MAGE does not require that all validation route through one kind of representation. It requires that the obligation and the evidence be adequate to the claim.

4.3.2 Build the Oracle

An oracle is whatever supplies the judgment against which the observed result is evaluated. An oracle is stronger when its judgment is sufficiently independent of the implementation being judged and explicit enough that its verdict has a stable meaning. Sometimes that oracle is a simple property: the output is an ordered permutation of the input. Sometimes it is a type or schema. Sometimes it is a reference implementation. Sometimes it is a human rubric.

SOFTWARE ENGINEERING

Inset — The oracle problem

Software testing has a longstanding asymmetry: executing a program can be much easier than deciding whether the result is correct. Testing research calls this the oracle problem ¹1. Earl T. Barr et al., “The Oracle Problem in Software Testing: A Survey,” IEEE Transactions on Software Engineering 41, no. 5 (2015): 507–25.. An expected output supplies an easy oracle for some cases; complex behavior may instead require properties, reference implementations, metamorphic relations, models, runtime evidence, or human judgment.

Commodity implementation widens the asymmetry. Agents can cheaply produce implementations, variants, and test inputs, but producing more candidates does not supply an independent basis for judging them. As generation becomes cheaper, the engineering bottleneck moves toward stating what must hold and constructing evidence capable of distinguishing acceptable realizations from unacceptable ones.

Existing behavior can stand in for a surprising amount of written specification. In a compatibility port or a structure-preserving migration, a reference implementation supplies an executable oracle: challenge a new realization with the same inputs and compare it against known behavior. Tests, benchmarks, compatibility suites, and production traces close the target further. The implementation problem may stay enormous, but much less of the engineering question remains open.

Explicit models matter because they can supply oracles for properties that do not exist at the level of one input/output example. A state machine can define legal transitions; an architectural graph can define permitted edges; a performance model can define an acceptable bound. The same representation that helps an agent reason about the system can therefore become input to an independent validator. Modeling enlarges the semantic reach of an oracle, but an oracle need not come from a model.

This is where generative validation becomes powerful. An example test pins one point: given this input, expect that output. A property states a law over a domain and lets a generator search for a counterexample. A stateful model can extend the same idea over sequences; a bounded concurrency model can extend it over interleavings. The useful progression is not "simple test to sophisticated test." It is from one known case to a claim over a space. Figure 4.3-1 draws the difference.

A failing example invites a local repair, because the evidence names one point: patch the branch that makes that input pass and the example goes green. A broader property makes that repair easier to falsify if the underlying class remains open — the generator keeps drawing neighbours that still exercise the law, so a branch-cut that satisfied one input fails the next. When the defect exposes a general law, preserve the law rather than only the example that revealed it.

The techniques that generate evidence this way share one loop — generate, execute, judge, shrink or diagnose — and differ in the generator that makes the inputs and the oracle that judges them. None is a maturity rung. Choose the generator and oracle that match the property you are trying to falsify (Inset 1 lays them side by side).

SOFTWARE ENGINEERING

Inset — Example, property, fuzzing, model-based: what changes?

Four ways to produce evidence, one shared loop — generate → execute → judge. They differ in where the inputs come from, where the verdict comes from, and what each is best at.

Table 4.3-1.

Technique	Inputs come from	Oracle comes from	Best at
Example test	engineer-chosen examples	the expected output, written down	known cases, regressions
Property test	an authored input domain	an invariant the output must obey	laws over many valid cases
Fuzzing	mutation and adversarial generation	a robustness contract, plus richer auxiliary oracles	malformed and edge inputs
Model-based / stateful	model-generated actions and states	an explicit behavioral model	sequences, protocols, state

Read each row left to right: the oracle defines what counts as success; the generator determines how the technique searches for evidence. The boundary is not even sharp: some systems combine an explicit input-language grammar with semantic constraints, generating high-diversity inputs while keeping tight control over what each one means ²2. José Antonio Zamudio Amaya et al., “FANDANGO: Evolving Language-Based Testing,” in “Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2025),” special issue, Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2025) (New York, NY), 2025, https://doi.org/10.1145/3728915. — a hybrid that sits between the property and fuzzing rows.

These are not rungs on a maturity ladder. Choose the technique whose generator and oracle match the engineering claim.

4.3.3 Generate Falsifying Evidence

Let the engineering claim choose the search. Not every obligation wants generated test inputs, and not every consequential property wants formal verification. Use the cheapest mechanism that can genuinely falsify the claim. Figure 4.3-2 sorts the claim kinds.

Start with prevention. If the forbidden state can be removed structurally, remove it. DocAble's pervasive work-item ownership rule is enforced by a database compare-and-set: an update succeeds only while the row remains in the expected prior state. Concurrent claimants race on the same transition, and only one can win. For that local ownership property, the runtime constraint can enforce the required transition directly; a temporal specification would answer a broader question than the one being asked.

When the property lives in interleavings, reduce the relevant state until it can be explored. DocAble's in-flight lease has this shape: a worker can appear stale and be reclaimed, another worker can acquire a fresh epoch, and the first can later wake and attempt release. The ownership question does not require the rest of the implementation. A reduced transition model retains only lifecycle state, lease epochs, reclaim, release, and the variables needed to state the invariants.

A small explicit-state checker exhaustively explores the resulting bounded state space. Separate checks compare selected production paths with the abstract model. These establish different things: exhaustive exploration searches the bounded model; the implementation checks provide evidence of correspondence. They do not establish formal refinement.

Some obligations cannot be falsified by a finite bad state. DocAble's serverless recovery path carries the temporal requirement that every submitted job eventually reaches a terminal state. A finite test can show that one execution terminated; it cannot show that no fair execution can remain stranded forever. For such liveness properties, DocAble uses small TLA+ specifications and TLC to reason about the temporal model. The representation and its checker answer a different question from the database CAS and the finite-state safety checker.

The three cases make the rule concrete: make violation impossible when the action space can be closed; exhaustively search a bounded model when the risk lives in finite interleavings; use temporal model checking when the obligation ranges over executions. None is automatically stronger engineering. Strength means adequate evidence for the claim that matters.

When a generated input exposes a defect, fix the stable obligation rather than merely the seed. The durable repair should close the class of behavior exposed by the counterexample whenever that class can be stated. A one-byte crash may reveal a parser invariant; a bad transition may reveal a missing state rule; a valid-but-unusual producer may reveal that the authored input grammar was incomplete.

Where available, real producers are valuable sources of dialects and edge cases that a synthetic generator may miss. Build richer synthetic generation when the engineering claim justifies the additional model and upkeep.

Three properties, three mechanisms

• Single ownership. The property is local enough to encode structurally. A PostgreSQL compare-and-set admits the ownership transition only while the row remains in its expected prior state. Concurrent claimants cannot both win.
• Lease fencing. The property lives in interleavings. DocAble maintains a reduced executable transition model and exhaustively explores its bounded reachable state space; selected runtime paths are separately checked against that model. Turning off the epoch fence produces counterexamples; the production configuration produces none within the explored bound.
• Eventual termination. The property is temporal. A serverless job must eventually reach a terminal state even when individual pushes are lost. A TLA+ model states that liveness obligation and can expose the stranded-job execution when the recovery sweep is removed.

The important difference is not the tool. It is the shape of the property.

4.3.4 Name the Obligation Set Before Claiming Coverage

Coverage answers a question about a population; the population must be named before the percentage has engineering meaning.

Ordinary test coverage starts from the implementation, or from the tests that already exist. It can tell you a line was never executed. It cannot tell you that an important behavior has no test at all, because nothing first named that behavior as an obligation. Implementation-derived coverage cannot reveal an obligation that was never represented in the population being measured.

Explicit models can supply the missing census. A state model enumerates the transitions that require evidence. An architectural model enumerates the forbidden or permitted edges. An error model enumerates the failure paths. A requirement model enumerates the claims that must be discharged. Derive that set from the models — every seam that owes a fuzzer, every failure edge that owes an injection test, every invariant that owes a checker — and a missing test becomes a named finding rather than an absence nobody notices.

From there, the assurance sequence is straightforward. Figure 4.3-3 lays it out: name the model, derive the obligations it implies, take the census, choose evidence appropriate to each claim, and only then claim coverage against that set.

With the census in hand, a high aggregate percentage stops being reassurance and becomes a place to look: this invariant has no exercising test.

4.3.5 Did the Search Cover the Claim?

Generative validation adds an honesty question that a small example suite can often avoid: did the campaign search the semantic region the claim is about? Code coverage answers where execution went. Input-space coverage answers what kinds of cases the generator produced. Neither alone proves the relevant obligation was exercised.

Where traceability exists, a more semantically targeted question becomes possible: which model claims were actually exercised? Follow an invariant, transition, or architectural relation to the code that realizes it, then ask whether the campaign reached that implementation under evidence relevant to the claim. A high aggregate percentage can then become a named gap: this invariant has no exercising test. The degree question — how much coverage is enough — belongs to the metrics treatment in Operating MAGE, which owns the discipline to measure one level deeper than a raw percentage.

Coverage remains evidence about the search, not proof of correctness. Its purpose is to keep claims such as "we fuzzed it" or "the model is tested" from becoming ceremonial. Figure 4.3-4 draws the loop: a generator makes inputs, the system runs, an independent oracle judges each outcome, a counterexample feeds back to shrink or diagnose, and coverage asks whether the search reached the claim before refining the generator.

4.3.6 Give the Verdict the Right Consequence

Validation may report or gate. Where a verdict should control admission, place that authority outside the producer's discretion. At consequential boundaries, consider re-deriving evidence whose freshness or independence matters to the admission decision rather than relying automatically on an earlier marker. A fuzz campaign may run nightly and report counterexamples without controlling merge; a cost validator may stay advisory; a security invariant may deserve immediate refusal. Authority is a separate design decision from evidence quality.

When such a campaign carries gating authority, the environment evaluates the obligation rather than relying on the producer's previous report.

4.3.7 Two Boundaries for Evidence

Part III gave a placement rule for authority: evaluate an obligation at the earliest boundary where it becomes legible and enforceable. That catches a problem close to its cause. A malformed brief should be rejected before an agent spends an hour acting on it. A structural violation visible at compile time should not wait for deployment. Early evidence shortens the feedback loop and keeps later work from compounding a defect that was already knowable.

Consequential work often deserves a second boundary: re-evaluate at the last safe point before the consequence becomes difficult to reverse. The two rules do not oppose each other. They answer different questions. The first asks: when can this property first be decided honestly? The second asks: what is the last point at which stale or invalid evidence can still be caught before the consequence?^** The security analogy is time-of-check to time-of-use (TOCTOU): a property established at one instant may no longer hold when the protected action occurs because relevant state changed in between. The problem here is broader than the classical TOCTOU race, but the engineering instinct is the same. Early checks establish defects cheaply; a consequential boundary may still need fresh evidence about the state actually being admitted.

Figure 4.3-5 draws the span between the two.

The second check is not a substitute for the first, and it need not repeat every earlier check. Where a second boundary is warranted, re-run or otherwise re-establish the evidence whose freshness matters to admission. A test result recorded hours ago describes the revision that produced it. A review verdict describes the change that was reviewed. A deployment rehearsal describes the configuration it exercised. If relevant state can change before admission, the evidence can cease to describe the artifact now crossing the boundary — a recorded claim is a statement about the past, not the present, and it rots as sibling work churns the ground under it.

Done is a claim, not a stored fact. At a consequential boundary, ensure that the evidence still justifies the consequence; where freshness cannot otherwise be established cheaply, re-derive the relevant evidence rather than trusting a stale green checkmark. The gain compounds with velocity: the more often a system ships, the more often an un-gated build reaches someone, so a cheap re-check at the last safe boundary is worth more, not less, as release frequency rises.

4.3.8 Why Abundance Changes the Economics

None of these techniques is new. Property-based testing, fuzzing, static analysis, model-based testing, independent review, and automated admission all predate coding agents. What changed is the relative price of implementation and inspection. When implementation was scarce, human attention could sit close to every change. When implementation becomes abundant, repeatable assurance mechanisms become increasingly valuable because human inspection does not scale with implementation volume.

The engineer does not disappear from validation. Human judgment moves toward the decisions for which it has the highest marginal value: choosing obligations, designing representations, selecting evidence, calibrating validators, deciding which verdicts deserve authority, and resolving the cases the environment cannot decide honestly. The old techniques become more central because the economics around them changed.