The verification ladder
You cannot verify against intent. So you build a ladder of proxies and stay honest about which rung you are on.
First, two words that get used as synonyms and are not. Verification: does the artifact satisfy the specification? A relation between two formal objects — mechanisable. Validation: is the specification the one we wanted? A relation between a formal object and a human intention — not mechanisable, only elicitable.
Almost all the risk is validation risk. Almost all the tooling built is verification tooling.
- Round-trip equivalence checking. Formalise, back-translate to natural language, re-formalise, then machine-check the two formalizations for logical equivalence. Divergence triggers stage-level diagnosis and a scoped repair targeting only the failing step.
- Golden cases. Curated input/output pairs with a stated rationale each. Authored by the intent owner, never derived from the rule — a test derived from the artifact tests nothing.
- Property-based testing. Golden cases assert points; properties assert invariants over a space. Shrinking to a minimal counterexample is what makes a failure actionable.
- Differential testing. Old version against new on historical data. Artifact against the incumbent system. Production implementation against a reference model.
- Counterexample generation. Ask a solver for an input where two versions differ. Are v3 and v4 equivalent? Does v4 strictly permit more? Is this branch reachable at all?
- Coverage, in two senses: structural (which rules were evaluated) and domain (which regions of input space map to which outcomes, and whether any region is unmapped).
- Formal methods, when affordable. Design-level specification is affordable and underused; code-level verification is not and you do not need it.
Rung 1 is stronger than "show a human the back-translation" — that framing undersells it. The published form removes the human from the comparison entirely, and evaluation on statutory text found rules failing the equivalence check show 1.4× to 2.5× more semantic drift than rules that pass. The signal tracks unfaithfulness rather than producing noise.
Whether humans shown a back-translation actually catch injected errors is, as far as anyone can find, unstudied. The warning that reviewers mistake a description for evidence remains an untested hypothesis. Say so rather than implying prior art.
Your generated-policy pipeline reports 95.3% compile rate and 98.9% negative-test pass rate. What is the number you should be worried about?
The rest of this lesson unlocks when you commit above.