Verification Engineering: How to Trust an AI System's Answer
A passed AI test proves one narrow property, not the whole task. The obligation ladder shows what to verify, test, prove and never assume.
Yash Sharma5 min readEvaluation and assurance
Research area 32: Verification, testing and formal-assurance engineering
In brief
- A passed AI test or proof proves one narrow, specified property, never that the whole task was done correctly.
- The obligation ladder climbs five independent checks, provenance to formal proof, before a claim counts as verified.
- Skipping independent verification means irreversible actions can run on evidence that was actually still unknown.
Verification, testing and formal-assurance engineering decides whether an AI system's output can be trusted before it acts, not whether it merely looks right. A passed proof, test or green checkmark is evidence about one narrow obligation examined, never a certificate the whole task was done correctly. A single all-purpose verification layer buys one badge that can be wrong.
What it is
Verification asks whether an artifact satisfies one specified property under stated assumptions. Validation asks whether that property is the one the business needed answered. Testing samples behavior on selected inputs. Formal proof establishes a proposition inside a defined logical system and trusted computing base, the parsers, translators and environment assumptions it depends on without re-checking them. Ask which of the four was actually done.
A check examines one obligation, not the whole claim: a passing result means this property held, never this is correct. The checker must be independent of the generator, since the same model grading its own answer twice is not independent evidence, and treating a classifier's opinion as proof is the most common category error in how enterprises talk about AI verification. Every result comes back verified, rejected or unknown, never folded into pass or fail.
Production systems increasingly generate their own proofs and tests, and a checker that passes something defective looks identical to one that caught a real error. A 2026 benchmark study of Lean, a formal proof language, examined five theorem proving benchmark families and found 4,833 checker flagged issues, of which only 398 were mechanically certified as real defects. Two frontier models triaged a set of 92 problems with precision and recall of .24 and .91 for one, and .30 and .82 for the other, figures specific to that sample, not a general defect rate. This does not prove a universal detection and repair system exists, only that a passed check is not proof of task correctness.
The architecture
The clearest way to build this is what I call the obligation ladder: five independent checks, each discharging one narrow obligation, climbed in order before a claim counts as verified.
The first rung checks provenance: does the source exist, is it the right version, does it match what it was captured at. The second checks structure: does the artifact parse, do typed fields, entity, amount, unit, date, line up as claimed. The third independently recomputes any objective quantity on a separate calculation path, since a correct sum built on a swapped entity is still wrong. The fourth tests behavior with executable tests and meaning-preserving transformations that should not change a correct answer. The fifth applies formal reasoning only where the property and trusted computing base are explicit enough to state, since a sound proof of a mistranslated program does not rescue the mistranslation.
Two failure modes recur: a precondition no real input can meet makes any proof built on it technically true and practically empty, and two checkers can appear to agree while sharing the same blind spot, since correlated checks are not independent evidence.
The ladder's output is never a single green badge, only a record of which obligations were verified, rejected with a witness, or came back unknown. An irreversible action should require its obligations to clear first, since no rung run afterward can undo an effect that already happened.
Ownership belongs with a team structurally separate from whoever builds the system being checked, since the same group cannot control both the checker and what it checks. Fund protected test infrastructure the system cannot modify in advance, an independent recomputation path for any quantity a decision depends on, and testing the checker against artifacts invalid but polished, and valid but unusually formatted. Measure obligation level outcomes, not badge pass rates, and treat a rising unknown rate as information, not a failure to suppress.
Two decisions belong to the executive alone: the acceptable balance between false acceptance and false rejection for a workflow, set before results come in, and what counts as the trusted computing base for an irreversible action, the parsers and environment assumptions accepted without re-verifying them. Governance should version the model, prompt, tool, policy, data and environment behind every acceptance claim, since any one changing can invalidate evidence that still looks unchanged.
What it is worth
Money and risk show up in three places: engineering time chasing a badge instead of semantic correctness, downstream cost when an accepted error passes silently into a decision, and exposure when an irreversible action runs on evidence that was actually unknown. On illustrative figures alone, a 10 percent prior rate of invalid artifacts with a checker at 90 percent sensitivity and 95 percent specificity leaves a residual chance an accepted artifact is still invalid of roughly 1.2 percent, specific to that scenario, not a measured result. With zero observed failures across 30 independent trials, the honest upper bound on the true failure rate still sits close to 9.5 percent, not zero.
Measure obligation level verified, rejected and unknown rates on a frozen gold set, at matched cost, before and after, rather than an aggregate pass rate that can hide the failures that matter most. The 2026 evidence assembled here supports that independent checks catch real specification defects and real verifier shortcuts. It does not yet support a dollar figure, a return percentage, or a claim that any detection and repair system has been proven, end to end, to reduce incidents.
Questions leaders ask
- What is the difference between verification and validation in AI systems?
- Verification checks whether an artifact satisfies one specified property under stated assumptions, such as a proof, a schema or a recomputed total. Validation checks whether that property is actually the one the business task needed answered. A system can pass every verification check and still have validated the wrong requirement, which is why leaders should ask which of the two was done, not only whether something was checked.
- Can a formal proof guarantee that an AI generated program or answer is correct?
- No. A proof only guarantees that a stated property holds inside a defined formal system and trusted computing base, which includes the parser, translator and environment assumptions behind it. A 2026 study of Lean proof benchmarks found thousands of checker flagged issues where mechanically accepted proofs still sat on defective specifications, and a sound proof of a mistranslated intent does not repair the mistranslation underneath it.
- Why can two independent looking checkers still make the same mistake?
- Because agreement is not evidence of independence. When a generator and its checker share training data, a prompt or the same underlying model, their errors can move together, and two checkers with the same modest miss rate can have a joint miss rate anywhere from zero up to that same rate rather than the lower number independence would suggest. Test checkers against genuinely different evidence channels before trusting their agreement.
- Should an AI system verify its own output?
- Not as the only evidence. A self-check can catch simple errors, but asking the same model to grade its own answer twice is not independent verification, since both calls draw on the same training and the same blind spots. The obligation ladder treats a self-check as one input at most, never as the checker of record for a decision that carries real consequences.
- What should never be reported to an executive as a single pass or fail number?
- A single green badge covering an entire AI task. The obligation ladder's real output is a record of which specific obligations were verified, which were rejected with a witness, and which came back unknown, and collapsing that record into one pass or fail figure hides exactly the unknown cases where a human decision is still required.
