When Does Verification Quality Determine Whether AI Automation Works?

Sources#

• Antaeus: Hunting Repository-Level Logic Vulnerabilities via Context-Grounded LLM Reasoning

Short answer#

Verification quality determines whether AI automation works when the AI's output is cheap to generate but expensive, dangerous, or impossible to trust by inspection. In that regime, generation is not the product. A verified artifact is the product.

This is the operational form of the The Verifiability Thesis: traditional software automates what can be specified; LLM systems automate what can be verified. The better the verifier, the more autonomy can move from "assistant proposes" to "agent searches." The worse the verifier, the more the system collapses back into human review, rubber-stamping, or unsafe volume.

The verification-quality ladder#

1. Perfect mechanical verifier: automation becomes search#

AI-Driven Formal Proof Search is the cleanest case. The agent emits Lean code; Lean mechanically checks every definition, theorem, and proof tactic. A proof is accepted only when the compiler reaches no pending goals, with no sorry and no disallowed axiom injection. That converts hallucination-prone mathematical prose into a binary artifact: accepted or rejected.

In this setting, verification quality determines success almost directly:

• The verifier is sound enough to reject fake proofs.
• The feedback is local enough to guide the next edit.
• The check is cheap enough to run inside the loop.
• The accepted output is valuable enough to send to humans for structural review rather than line-by-line truth checking.

The verifier is not just a final gate. Lean compiler errors ground the next agent turn. That is why Agentic Loops Overtake Bespoke Systems matters: DeepMind's basic loop of independent prover agents matched the elaborate evolutionary/AlphaProof apparatus on all 9 solved Erdos problems, though at higher cost on the hardest ones. The loop worked because the verifier was strong enough to make dumb search productive.

The important caveat is Lean's own frontier: mathlib maturity gates what can be reached. A perfect verifier does not make every domain ready. It only makes automation work where the target can be formalized and the supporting library exists.

2. Strong but incomplete verifier: automation works, but infrastructure becomes the bottleneck#

Software engineering sits below Lean on the ladder. Tests, CI, lint, typecheckers, specs, and code review are real verifiers, but they are partial. They catch regressions, style errors, type violations, obvious bugs, and spec drift; they do not prove the full product is correct.

That is why Verification as the New Bottleneck is the org-level consequence of the The Verifiability Thesis. Once Claude Code makes coding cheap, the scarce resource is confidence that the change is correct. The bottleneck moves from writing code to verification, review, and maintenance.

The automation works when verification shifts left:

• Tests are written before or alongside code, so TDD loses its old "tax."
• Specs live in the repo, so agents can check for spec drift.
• CI/build capacity keeps up with the new volume.
• Human review is reserved for legal, risk-tolerance, and trust-boundary decisions.

The failure mode is not "AI cannot code." The failure mode is that code volume outruns verification capacity. If PR cycle time does not fall, Verification as the New Bottleneck says to break the funnel apart: it may be CI/build infrastructure jamming under agentic throughput, not low AI adoption.

3. Empirical verifier: automation works if reality gives fast feedback#

LLM-Driven Vulnerability Research is a messier but important case. The agent is not proving theorems. It is searching code, hypothesizing vulnerabilities, running programs, debugging, generating PoCs, and producing reproduction steps. The scaffold is simple: isolated container, project source, a paragraph-level prompt, parallel agents focused on different files, and a final validation agent filtering severity.

Here verification quality is not mathematical soundness. It is empirical confirmation:

• Can the agent reproduce the crash, exploit, or control-flow hijack?
• Can it produce a PoC and steps another reviewer can run?
• Can a validation pass separate critical findings from junk?
• Can the workflow filter minor issues before humans drown in volume?

The page's evidence supports both sides. The scaffold found major bugs, including RCEs, and Mythos Preview moved from finding vulnerabilities to chaining working exploits. But the need for file ranking, reproduction, final validation, severity review, safeguards, and controlled release is itself the point: in high-risk domains, verification quality determines whether automation is defensive leverage or unreviewable dangerous output.

Compared with Lean, vulnerability research has weaker verification but more contact with executable reality than fuzzy judgment tasks. That puts it in the middle: automation can work, but only when the scaffold forces concrete artifacts that can be rerun and checked.

3b. No executable verifier at all: the fallback is structure plus peer comparison (added 2026-09-23)#

Rung 3 assumes the agent can run something — reproduce the crash, produce a PoC, rerun the artifact. A whole class of security work cannot. Antaeus (Antaeus: Hunting Repository-Level Logic Vulnerabilities via Context-Grounded LLM Reasoning, empirical) hunts access-control and information-exposure flaws in C/C++ repositories and assumes no exploit inputs, no runtime traces, and no execution environment — the vulnerability is a missing guard, and there is nothing to reproduce. This is the interesting case for the ladder, because it shows what a system builds when rung 3's empirical check is unavailable and rung 4's "stay assistive" is not an acceptable answer.

Two substitutes, and neither is a verifier in the rung-3 sense:

1. A structured output schema as a claim-grounding device. The model may not return a verdict; it must name a security-sensitive sink, enumerate the safety conditions that sink requires, mark each locally_satisfied true or false, and attach a code-grounded justification. A finding is accepted only when the judgment and its supporting evidence are right, so a correct label with inconsistent reasoning is discarded. That is actionability and review filtering bought without soundness: nobody has verified the condition holds, but a reviewer is told which predicate to check rather than handed a binary verdict to re-derive.
2. Peer comparison inside the same corpus, standing in for ground truth. A flagged condition is retained only if it is distinctive among structurally similar sinks in the same repository, and pruned when the same unsatisfied condition recurs uniformly — on the premise that uniformity is the project's norm, not a bug. Sink identifiers are embedded with UniXcoder, condition texts with a sentence-transformer, thresholds calibrated per repository. It removes 25–27% of false positives while dropping zero true positives, at no model cost.

The result is what this ladder predicts for a rung with no reliable rejection: automation works, and it works by volume rather than by trust. 20 of 35 known CVEs detected and explained, against 1,732 findings — one confirmed bug per ~87. Compare rung 1: Lean accepts nothing false. Here nothing is rejected on truth at all, only on typicality, so the human reviewer stays in the loop at full load and the system's contribution is having narrowed 186,859 functions to 6,112 and attached an argument to each flag.

The rung's rule, then: when the verifier cannot exist, buy actionability and filtering instead of soundness, and price the residual human attention explicitly. The design does not raise autonomy — it lowers the cost of the review that autonomy would have needed anyway, which is the only move available below rung 3.

4. Noisy verifier: automation remains assistive#

The The Verifiability Thesis allows that almost everything can become verifiable "to some extent," even soft domains via LLM-judge councils. But "to some extent" is not enough for full delegation. A noisy verifier may improve ranking, triage, or drafting, but it cannot carry the same autonomy load as Lean.

This is the dividing line: when the verifier cannot reliably reject bad outputs, automation must stay closer to human judgment. Otherwise the system only scales plausible-looking errors.

When verification quality is decisive#

Verification quality becomes the deciding variable when four conditions hold:

1. Generation is abundant. The agent can produce many candidate patches, proofs, exploits, reports, or plans cheaply. This is true in Verification as the New Bottleneck, AI-Driven Formal Proof Search, and LLM-Driven Vulnerability Research.
2. The output has external correctness. A proof either typechecks; a test either passes; an exploit either reproduces; a patch either preserves behavior. Taste alone is not the target.
3. Bad outputs are costly. Wrong proofs waste expert attention; bad code increases maintenance; unvalidated vulnerability output can create security risk or disclosure overload.
4. Feedback can enter the loop. The verifier must produce a signal the agent can act on, not merely a late human verdict.

When all four hold, improving the verifier often matters more than improving the prompt. The agentic loop becomes: generate, check, learn from the check, repeat. If the check is reliable, the loop compounds. If the check is weak, the loop compounds noise.

What verification quality consists of#

The sources imply five dimensions:

• Soundness: Does acceptance mean the artifact is actually valid? Lean is the high-water mark.
• Coverage: Does the verifier check the part of the task that matters? Tests and CI are useful but incomplete; mathlib maturity limits formal proof search.
• Actionability: Does the failure signal guide the next attempt? Lean compiler errors do; vague human review often does not.
• Latency and cost: Can verification run inside the agent loop? If it is too slow or expensive, it becomes a final audit instead of a search primitive.
• Review filtering: Does the verifier reduce human work to the outputs worth reviewing? AI-Driven Formal Proof Search explicitly frames formal verification as a filter for determining which proofs merit human review; LLM-Driven Vulnerability Research uses validation to filter findings.

Bottom line#

AI automation works when the verifier is good enough to turn model output into a search space with reliable rejection. Lean shows the ideal: the verifier is sound, local, cheap, and loopable, so a simple agentic loop can overtake bespoke machinery. Software engineering shows the practical middle: tests, CI, specs, and review make automation useful, but verification infrastructure becomes the bottleneck as code volume rises. Vulnerability research shows the dangerous middle: empirical reproduction and validation can make automation productive, but weak verification turns scale into risk.

So the rule is simple: raise autonomy only to the level your verifier can support. Below that line, use the model as an assistant. At that line, use it as a search process. Above that line, the verifier, not the model, is the system's load-bearing component.

Related#

• The Verifiability Thesis
• Verification as the New Bottleneck
• AI-Driven Formal Proof Search
• Agentic Loops Overtake Bespoke Systems
• Lean
• LLM-Driven Vulnerability Research
• RSI Autonomy Levels (B0–L5) — this page's ladder applied to self-improvement rather than to task automation, and it reaches the same rule from the other side. A September 2026 survey finds L2 is the established frontier in all four domains it examines — science, embodied intelligence, software engineering, healthcare — and L2 is exactly the highest level reachable while the acceptance criterion stays external and cheap to apply. The domains diverge above and below that line by validation cost: software engineering alone reaches L3 because the artifact and its verifier are both executable, while healthcare and embodied intelligence stall because outcomes are delayed, confounded, or not resettable. "Raise autonomy only to the level your verifier can support," restated as a survey result