4.6 Validation with Agents
Most tests reproduce a dot. You pick an input, you write down the output you expect, and the test asserts the two match. That is honest work, of course, and it catches a great deal; but it says nothing about the input sitting right next to the one you chose. There is a different move, and once you see it as a single move it turns out to name three techniques at once: generate inputs and try to falsify a specification the model supplies. Property-based testing, fuzzing, and the synthesis of fuzzing with model-based engineering are the same move three times. They differ on what the specification is, on what it means to fail it, and on how the inputs get made — and drawing those three axes sharply is what keeps the family from collapsing into a vague "testing with randomness."
That move is the whole book worn as a test. The specification the generator hunts is a model — the Modeling Thesis, that the system's correctness lives in an explicit model and not in prose. And the generator re-hunts a counterexample on every change — the Alignment Thesis, that the environment keeps re-checking the agent's work against that model automatically, forever, rather than trusting a one-time review. A generative-validation test is those two theses standing in one place: a compact model, and a machine that never stops trying to break it.
4.6.1 One move, three specifications
Table 4.6-1 lays the family out on one page. I suggest reading each row left to right — oracle, then failure, then generator — because the oracle is what the technique is and the generator is only how it gets there.
| Technique | What the oracle is | What counts as a failure | How inputs are generated |
|---|---|---|---|
| Property-based testing | A declared invariant the author writes — a law the output must obey for every input: parse-then-serialize returns the original; a remediated document contains no less content than the original; a sort yields an ordered permutation. | The stated law is false on some generated input. | A structured generator synthesizes well-typed domain values; on a failure it shrinks the input to the smallest one that still breaks the law. |
| Fuzzing | An implicit total-function contract — "never crash, never corrupt," and "reject cleanly whatever the format forbids." The oracle is coarse but real: the process survives, and the output re-parses. | A crash, hang, resource blow-up, or silent corruption on adversarial or spec-edge input, even where no explicit law was stated. | Malformed or adversarial bytes — truncations, bit-flips, corrupted offsets, garbage appended — reaching inputs no well-typed generator would ever emit. |
| Fuzz + model-based engineering | The structured model itself — the same model the fleet reasons through — becomes the oracle. It names the stable point in the specification: the closed set of legal outcome classes, the invariant predicate, the state-transition table. | The generated input drives the model into a state it declares illegal — an outcome outside the legal set, a transition the table forbids, an invariant predicate that goes false. | The same adversarial generation as fuzzing, aimed at a model-declared surface: the model's own read entry point, a state machine's driving conditions, a flow between services. |
Three sharp distinctions fall out of that table, and stating them keeps property testing and fuzzing from blurring together.
First, oracle richness and input wildness trade off, and the third member refuses the trade. The richer the oracle, the tamer the inputs: a property test knows exactly what correct means, and yet it asks the question only of inputs a type would allow. The wilder the inputs, the coarser the oracle: fuzzing reaches bytes nothing else reaches, and yet it can notice only a crash. Fuzz-with-modeling is the synthesis that takes both halves: wild inputs, judged against a rich model-declared oracle. That synthesis is this book's thesis in miniature: the model supplies the oracle, and the search never stops hunting a counterexample to it.
Second, the word failure means different things, and conflating them is the classic mistake. For a property test, a failure is a stated law turning out false. For a fuzzer, a failure is the program leaving its safe envelope, crashing or corrupting, in a place where no law was ever stated. Blur the two and you get the two symmetric errors: a fuzzer that only checks for a crash when it should have been asserting an invariant, and a property test fed only tame inputs when the real risk was the malformed byte at the boundary.
Third, the specification's stable point is the bridge between fuzzing and the model. When a fuzzer finds a crash, there are two ways to fix it. You can patch the one input that broke — and leave every neighbouring input that would break the same way. Or you can trace the failure back to the point in the format's specification that the input violated, and fix that — so the fix covers every input the specification allows, not the single seed that happened to trip it. Fixing to the stable specification point is what promotes a raw fuzzer into a model-based one: the model is the stable point, written down.
4.6.2 The move: a generator hunts a counterexample to a model
Before the three members, the shared shape. An example-based test pins a single point: given this input, expect that output. A generative test does something else — it states the property the output must satisfy across the whole space of inputs, and hands a generator the job of hunting a counterexample. Where an example gives the machine one labelled dot to reproduce, a generative test gives it the law the whole space obeys and a search for the place the code breaks it.
That difference is exactly the one that matters against an agent. Faced with a failing example, an agent will do the locally-expedient thing: special-case the path that makes that input pass. The example goes green and the bug survives, now hidden behind a branch cut to fit the test. A property has no case to special-case. An agent that special-cases the one input sails through the example and straight into the law that the whole space of neighbours still has to obey. This is why the strategy that catches the class beats the one that catches the example, and why the generative family is the sharpest tool the lessons chapter reaches for when it says to pin the invariant, not the example. Figure 4.6-1 draws the difference.
4.6.3 Property-based testing: the invariant is the oracle
In property-based testing the author writes the law and the machine hunts the counterexample. The law is a statement about every output, not a single one: parse-then-serialize returns the byte-identical original; a remediated DocAble document contains no less content than the one that went in; a sort produces a permutation of its input in non-decreasing order. Each of these is a compact, checkable model of what a correct output looks like — a law, not a list. The generator synthesizes well-typed domain values across the space the law is supposed to hold over, runs the code, and checks the law. When the law breaks, the framework shrinks: it walks the failing input down to the smallest one that still breaks it, so the counterexample you get is minimal and legible rather than a thousand-node document with one bad byte somewhere inside.
The property is the Modeling Thesis worn as a test: a small statement the agent reasons over instead of enumerating cases it cannot hold in context. The generator is the Alignment Thesis, re-hunting a counterexample on every commit. In a real system this is no footnote technique. A property-based framework can run across every test project, and the discipline is to reach for it the moment a class's contract is expressible as a law rather than a list of examples. The counterexample it hands back is often a genuine defect the author never thought to write an example for. That is why you ask the machine to search the space instead of guessing at its corners.
Learn more about this governance mechanism: property-based tests.
4.6.4 Fuzzing: the contract is "never crash, never corrupt"
Property testing asks tame inputs a rich question. Fuzzing asks a coarse question of wild ones. The oracle is the implicit contract every input-parsing surface signs whether or not anyone wrote it down: do not crash, do not hang, do not corrupt, and reject cleanly whatever the format forbids. A malformed DocAble upload — a PDF truncated mid-object, a slide deck with a corrupted offset table, a document with megabytes of garbage appended — is precisely the input a generator of valid documents will never produce, and precisely where the crash lives. The fuzzer mutates and adversarially perturbs its way into that space and watches for the process to fall over or the output to fail to re-parse.
The multiplier is discipline about the fix. When a fuzzer surfaces a crash, the temptation is to handle the exact bytes it found. The stronger move is to trace the failure to the point in the format's specification that the input violated, and fix that — because the specification is stable while any one producer's quirks are not, so a fix aimed at the specification point closes every input the format allows, not the single failing seed. That is the discipline that turns a pile of one-off crash patches into a class of inputs handled once.
A campaign that merely runs has explored nothing, so the honesty layer matters: the host test-runner can auto-collect line and branch coverage over each fuzz campaign and track it against a baseline, so "we fuzzed it" becomes a claim with a number behind it rather than a vibe. That number is a saturation signal: the campaign has stopped finding new edges. Its deeper treatment belongs to the metrics chapter, which owns coverage.
Learn more about this governance mechanism: fuzz campaigns.
4.6.5 Fuzz + MBSE: the structured model becomes the oracle
This is the synthesis. Take the wild inputs of fuzzing and, instead of asking only "did it crash," judge the outcome against the structured model the fleet already reasons through. The model names the stable point in the specification: a closed set of legal outcome classes, an invariant predicate, a transition table. Point the malformed bytes at the model's own entry point, and classify what comes back against that declared set. A clean rejection of an illegal input is a pass — the model correctly refused it. An outcome outside the legal set — an unexpected exception, a silently corrupted structure, a state the transition table forbids — is a fail. The oracle is now as rich as a property test's, and the inputs are as wild as a fuzzer's. The trade-off the first two members lived under is gone.
Two instances make this concrete.
The first is the format model. Feed adversarial bytes to the structured document model's read entry point and sort the result into a small, closed set of legal outcome classes — parsed cleanly, rejected cleanly with a typed error, and so on. The set is the specification. An outcome the set does not name is the failure, and because the set is the model's own declaration rather than a hand-written assertion per seed, the same oracle judges every input the fuzzer can throw.
The second is the sharpest instance in the whole family, and it turns the fuzzer's usual approach inside out. Call it the producer-dialect corpus. Instead of mutating toward malformed bytes, round-trip a real document through a genuine third-party producer — a different office suite, a different PDF writer, a different export path — and let that producer's legal-but-unusual dialect be the adversarial input. Every producer emits its own accent within the format's grammar: unusual-but-valid object orderings, obscure-but-permitted structures, features the specification allows and your own writer never uses. Where the specification-point fix reasons inward from a failing seed to the stable rule it violated, the producer-dialect corpus reasons outward — it generates inputs that occupy the whole specification-allowed producer space, so the model is tested against the full breadth of what the format legally permits rather than the narrow slice your own tooling happens to emit. It is the family's most distinctive move, and it needs no mutation engine at all: the world's producers are the generator.
Harvest producers before you hand-roll a grammar. A grammar you write yourself covers the dialects you thought to encode. The format's independent producers — every rival tool that writes it — have already generated the legal-but-unusual space for you, a breadth no single authored grammar reaches. Reach for a from-scratch generator only where no real producer exists.
The synthesis reaches one level up when the specification is not a format but a concurrency invariant. There the "input" is an interleaving of concurrent steps, the generator is an interleaving-fuzzer or an exhaustive search over reachable states, and the oracle is the invariant predicate evaluated over the model's states — no two workers hold the same lease; a job never leaves a terminal state; a queued item is eventually served. The class of the invariant even picks the checker: a straightforward linear invariant earns a property test, while a hairy invariant over concurrent interleavings earns an exhaustive state search that walks every reachable combination. The payoff, learned the hard way, is that naming the invariant predicts where the bug is. Writing the predicate down forces you to state the exact condition that must hold, and the search then drives straight at the interleaving that violates it — a defect a strong-but-static unit suite walks right past. This is generative validation standing on the same invariants-over-models ground the rest of the book is built on.
4.6.6 Coverage: did we explore the spec-relevant space?
Once you have a generator, a new question appears that example tests never had to ask: did the campaign explore the space that matters, or did it just spin? The book already owns coverage — the metrics chapter develops it as a flagship, with the rule to measure one level deeper than the raw percentage — so this section adds only the one cut that is genuinely native to generation and hands the rest back.
The native cut is grammar coverage. Line and branch coverage measure the code the inputs reached. Grammar coverage measures the inputs themselves: did the generator exercise every production of the input grammar — every structural variant, every mutation kind, every dialect the corpus is supposed to contain? It is branch coverage moved to the input side, and it answers the question the gap analyses of a real fuzzing effort keep circling back to: is the corpus rich enough? A campaign that never generates a document with headers and footers, or never a cross-sheet formula, has a grammar-coverage hole no amount of line coverage will reveal, because the untested lines were never reached by any generated input in the first place.
For everything else, defer to the metrics chapter and close the loop. Line and branch coverage of the campaign is the saturation signal, and it is the honesty layer that keeps "we fuzzed it" from being an empty claim. But the coverage that ultimately matters for this family is model claims — did the generated inputs actually drive the invariants, transitions, and edges the model declares, measured as the metrics chapter's requirements-based coverage over the traceability graph? That is the connective tissue: the same "measure one level deeper" move the metrics chapter teaches, reused here as the saturation oracle for generative validation. Figure 4.6-2 draws the loop, closing on that coverage.
4.6.7 When to reach for which
The family gives a compact decision aid, and the axes of the opening table are the decision.
- A stated law over structured inputs — a round-trip, a content-preservation guarantee, an ordering — reach for a property test. The oracle is the law you can already write down.
- An untrusted-bytes boundary with a never-crash contract and no law worth stating per input — reach for a fuzzer, and fix its findings to the stable point in the specification, not the failing seed.
- A structured model with a declared legal-outcome set or invariant — reach for fuzz plus the model: point wild inputs at the model's surface and judge the outcome against its declared classes. When a real third-party producer exists, let its dialect be the corpus.
- A concurrency invariant — reach for the state-model variant: a property test for a linear invariant, an exhaustive search for a hairy one over interleavings.
All four are hard governance in the soft-versus-hard sense the lessons chapter draws: deterministic sensors, machine-read, re-run on every commit. They do not aim the agent and hope; they hold the line. A generator that re-hunts a counterexample every commit is the Alignment Thesis made mechanical — the environment refusing to trust the last green checkmark, and checking the model again, forever.
Step back from the fuzzer to the Part it ends. This one put the method to work end to end — the brownfield recipe, the skills that carry it, the transformations that move a legacy tree onto models, and the generative checks that hold the result. None of it came from a whiteboard; every move was forced by one real system under a real deadline. The next Part tells that system's story from the beginning.