Figure 27.2: The generator-and-gate loop at the frontier of verification
Figure 27.2 The generator-and-gate loop at the frontier of verification. A person
states the properties; the model drafts the spec or property tests; and a
deterministic checker (in accent) renders a verdict no fluency can charm. A pass
ends the loop; a failure returns a counterexample that drives revision, and the
generator may be wrong as often as it likes because the gate cannot be argued
with. The honest limit: it checks only the properties you actually stated.
