Draft, September 2026

Sections / 12

12. Verification moves from reading to running

In short

People reviewing formal artefacts miss errors, so verification should move from reading to running: a case corpus of inputs with known outputs that the agent runs its own document against, with results shown to someone qualified to judge them.

In the video · scene 13
The explainer video for the paper SaaS architecture when code is cheap

The weakest link in the schema-plus-review arrangement is the reviewer. A person confirming that a generated configuration is correct is reading a formal artefact and judging whether it matches an intent expressed in a document. The evidence on how well people do that is discouraging. In the Catala study of a formal language for statutory law, only 2 of 7 law graduates who had already confirmed a formalisation correct detected a seeded operator inversion (Catala). In a scalable-oversight study, reviewers checking model output reached 0.71 accuracy where the model alone reached 0.75 (scalable oversight, 2025).

Historical successes with executable formalism verified by running rather than by reading. Catala found a real defect in France's official benefits simulator by executing its rules against known cases. ISDA measures its executable regulatory rules by regulator acknowledgement rates, reporting 98.2% at one go-live and 100% at another (ISDA Digital Regulatory Reporting, undated industry report).

For a configuration language, this means the artefact that matters alongside the grammar is a case corpus: inputs with adjudicated outputs, which the agent runs its own document against. In an onboarding context that has a natural form. Given a configuration for a new customer, compute a result the customer already knows, such as a sample calculation or a worked example from their own records, and show it back. The configuration is then judged by its output rather than by its text, and the person reviewing it is judging something they are qualified to judge.

This loop is also where a language acquires its value. A language with no compiler is a notation. The loop back to a visible result is where the value sits, and a programme that builds the grammar without the loop has built the cheaper half.

Sources

  1. Catala
  2. scalable oversight, 2025
  3. ISDA Digital Regulatory Reporting