Verifiability engineering

Verifiability engineering is the practice of moving each property of a task toward the strongest evidence channel that its semantics allow, instead of asking whether a whole domain is "verifiable". Its tools are four moves — decompose, instrument, compile, and retain the residue honestly — and one selection rule, applied per criterion and per regime.

The wrong question#

"Can this domain be verified?" is often the wrong question; the better one asks which operations, claims, and sub-properties can be made more verifiable. A domain labeled non-verifiable is rarely so in principle. The label usually means that the cost of establishing ground truth is high, the criterion is inherently plural, or no sound automatic oracle is available at the granularity required, and each of those conditions attaches to a property, not to the domain.

Research quality is the standard example of a non-verifiable blob, and it is not one. Decomposed, "useful, honest, reproducible research" spreads across several strengths of evidence:

The work is to move rows up where the semantics allow and to be honest about the rest; Case D builds the full evaluator.

Four moves#

The framework names four moves:

1. Decompose: split vague quality into independently meaningful criteria.
2. Instrument: make the artifact emit tests, citations, provenance, state snapshots, uncertainty, and proof obligations.
3. Compile: translate criteria into deterministic, executable, or formal checks when the semantics permit.
4. Retain the residue honestly: use calibrated learned or human judgment for what cannot be compiled, and report its uncertainty, with a route to escalation.

SQLAgent, the text-to-SQL agent of Case C, shows all four. Decomposition splits "answers analysts' questions correctly and safely" into facets such as query interpretation, join reasoning, date semantics, ambiguity handling, refusal when a question is unanswerable, and permission compliance. Instrumentation adds pinned database snapshots, before-and-after state, and tool traces. Compilation turns correctness into execution against the snapshot, with semantic result-set equality and metamorphic tests, and permission compliance goes further: read-only credentials and row-level permissions make violations unreachable. Ambiguity handling and explanation quality remain, for a rubric-guided judge with SME adjudication of semantic edge cases. The design principle in one line: formalize access policy, execute semantic consequences, and reserve learned judgment for the residual problem of language and intent.

Decomposition is what makes the other moves possible, which is why a rubric matters beyond the judge prompt it feeds: the most valuable rubric is not merely a better prompt for a judge, but a decomposition that reveals which criteria can be compiled into stronger checkers. Instrumentation works on the evidence view, not on the model: evidence architecture can move criteria upward in evidential strength without changing the underlying model.

The strongest affordable mechanism#

For each criterion, ask five questions in order:

1. Can it be guaranteed by construction or formal verification?
2. Can it be checked by execution or direct state inspection?
3. Can it be decomposed into deterministic subclaims?
4. Does it require a calibrated learned judge?
5. Does it remain human-judgment territory?

The first "yes" names the strongest mechanism, and the order carries a rule: do not use a learned judge where an executor can answer the question more directly. A judge that reads SQLAgent's query and decides whether it looks right does, with error, what executing the query against the snapshot does directly.

The framework amends the rule for cost and for regime: choose the strongest affordable mechanism per criterion per regime, then deliberately use different mechanisms across development and certification when independence is valuable. Cost matters because training may need millions of evaluator calls where certification needs hundreds, so a cheap learned judge can serve development while execution plus expert sampling certifies the release. Independence matters because evaluators that share a model family, data, prompts, or evidence fail together: blind spots the optimizer found in development pass a certification channel that shares them. In the Studio, each criterion engineer chooses a mechanism for every channel the regime uses and records which of the four moves it made.

Record the chosen mechanism's rung in the verification hierarchy as a prior, not a certification; the validation profile replaces it with measurements.

Gold answers do not add a rung: a gold answer is a reference anchor, and whatever compares against it takes its own place in the order (The verification hierarchy explains why).

The card below is SQLAgent's "no unauthorized writes" criterion compiled as far as it goes: read-only credentials make writes unreachable, a snapshot diff and a trace scan check the rest, and the hierarchy prior reads "By construction". Switch to the grounded docs answer, whose mechanism is already a hybrid portfolio: citation existence moved to a deterministic check, while entailment stays with a judge at rung 3 of 4 (set the mechanism to Learned judge to see that rung). Ask which of its remaining subclaims could move as well, and what would stay with the judge.

Locate first, then choose a recipe#

The rule is locate first, instrument second. Before asking whether to use an LLM judge, place the problem on four axes: is the response space closed or open; is success externally verifiable or judgment-based; is the benchmark static or refreshed in versions; and is behavior single-turn or a stateful trajectory? Oracle strength is the bridge to the instrument, because it determines how high on the verification hierarchy the instrument can operate and how much calibration burden remains. Reading agent benchmarks applies the same axes to published benchmarks.

Once the problem is located, seven recipes give a reasonable starting architecture for the common locations:

One construct can land in several cells. Take whether an agent can produce a correct financial reconciliation: a multiple-choice version is scored directly but says little about real reconciliation work; a spreadsheet artifact can be highly verifiable if its formulas and balances execute; a written explanation of why a discrepancy matters needs judgment; and an agent that edits ledgers creates a trajectory problem, because an unsafe intermediate write matters even when the final balance is correct. The construct is related across all four cases; the evaluator architecture should not be the same.

Climb by redesigning the artifact#

The recipes take the location as given; verifiability engineering can change it. A research report that asserts "our method works" is hard to verify. Require the agent to emit a code artifact, an experiment manifest, raw metrics, seeds, ablations, claim–evidence pairs, and uncertainty annotations, and reproducibility and evidential support move up the hierarchy, even though research quality as a whole stays partly a matter of judgment. The same redesign works elsewhere: a coding agent can produce tests and proof obligations, a data agent before-and-after invariants, and a policy agent a log of decision-relevant evidence. Better evaluability can be an architectural property of the system, not only a post-hoc property of the benchmark.

The survey of recursive self-improvement (Chen, Wang & Qu, 2026, §6.3) reaches the same conclusion from its AI-scientist literature. Once writing a report is cheap, the expensive part is establishing which evidence each sentence depends on, and the survey names auditability as the new bottleneck; the responses it describes make claims auditable one at a time and scale each assertion's strength to its evidence, so that machine-written science is checkable by construction rather than after the fact.

What compiling cannot do#

A compiled check is faithful to the property it encodes, and that property is not the construct. A proof checker can be perfectly sound for the wrong theorem; a unit test can execute perfectly while omitting the behavior users care about.

Hence the question: when does increasing verifiability narrow the construct too much? The danger is that the checkable part quietly becomes the whole specification. A research evaluator that compiles citation provenance and artifact reproduction, then drops novelty and importance because they resist compilation, certifies reproducible research rather than useful research. The guard is to keep the smallest set of independently meaningful criteria that still reconstructs the expert decision with acceptable fidelity, counting the compiled criteria and the residue together, and to test that reconstruction against experts' holistic verdicts.

At the far end of the residue lies the non-verifiable frontier: creative writing, dialogue, research taste, and above all choosing research directions, where none of the workarounds, from meta-evaluation to claim-level auditability, is yet as reliable as execution feedback (Chen, Wang & Qu, 2026, §5.4). Self-improvement and evaluator co-evolution explains why the survey treats it as the binding constraint on every improvement loop.

In practice#

Climb one criterion at a time, for each regime that consumes it.

1. List the criteria and their regimes. Note which uses consume each criterion: development feedback, certification, production monitoring.
2. Ask the five questions in order. Stop at the first mechanism that can answer and that the regime can afford.
3. If the answer is weak, change the artifact. Ask what the system could emit to let a stronger mechanism answer: claim–evidence pairs, tests, manifests and seeds, snapshots, traces, or proof obligations.
4. Compile what the new evidence allows. Turn deterministic subclaims into checks, consequences into execution, and forbidden states into structural controls.
5. Keep the residue, with its uncertainty. Route what remains to a calibrated judge or an expert panel with abstention and escalation, and report its error separately.
6. Split development from certification. Where the development signal is optimized against, certify with a different mechanism and measure how often the two miss together.
7. Test the decomposition against experts. On a sample, compare a holistic judge, a decomposed rubric judge, and the hybrid stack on per-criterion error, nuisance invariance, and decision flips, not only agreement.
8. Record each choice on the criterion card, with the hierarchy family as a prior and the blind spots.

The artifact is a mechanism map: one row per criterion and regime, giving the mechanism, its hierarchy family, the evidence it needs from the artifact, and the residue left to judgment.

Common failure modes#

• A judge where an executor can answer — an LLM judge reads code or SQL and decides whether it looks correct → execute it against tests or a pinned snapshot, and judge only what execution cannot settle.
• One mechanism for every regime — the judge that guides development also certifies the release, so the blind spots the optimizer found pass certification too → certify with a different mechanism and measure the coupling. See common-mode assurance.
• Evidence that can be faked — the artifact now emits citations, and a format check accepts confident fabrications → compile the check against the evidence itself: the cited passage exists, in the current version, and supports the claim. See grader gaming.
• The construct compiled away — the checkable criteria become the whole specification, and scores rise while expert verdicts do not → keep the residue in the instrument and test the decomposition against holistic expert verdicts. See Goodharting.

Check yourself#

Analyze. Decompose "safe autonomous research" into sub-properties, and place each at the strongest channel its semantics permit.

Hint

Start from the research-quality table, then add the safety properties. Ask which actions can be removed or gated by construction, which can be checked on the trace, and which need judgment.

Evaluate. To make "explanation quality" verifiable, a team replaces its judge with a deterministic check that every explanation cites at least two documentation passages. Evaluate the change.

Hint

Citation count is easy to compile and easy to game, and the framework lists superficial citation density as a nuisance for a research-quality judge, not a facet. If the check no longer reconstructs expert verdicts, it has narrowed the construct, and the residue still needs a calibrated judge.

Create. Redesign an open-ended evaluation so that at least two formerly judgment-based criteria become executable, without collapsing the construct.

Hint

Change what the system must emit, such as claim–evidence pairs, a manifest with seeds, or before-and-after invariants. Then write the check each new artifact enables, and name the residue that still needs judgment.

Further reading#

• Mechanism families — what each family can establish, and how hybrid portfolios route criteria.
• Anchors and evidence views — the evidence view that the instrument move changes.
• Guarantee before you estimate — the first of the five questions: making failures unreachable.
• Case D: autonomous research agent — verifiability engineering applied to research quality.
• Chen, Wang & Qu (2026), "Recursive self-improvement in AI: From bounded self-refinement to autonomous research loops" — §5.4 and §6.3 on the non-verifiable frontier and auditability.