The Verification Frontier: Proof, Oversight, and Trust After Capability

The previous chapter asked what a capability result actually measures. This chapter asks the question that follows: what evidence would justify acting on a result? A model can produce an answer, proof sketch, program, design, biological hypothesis, or market forecast in seconds. Production is not acceptance. Between the two lie specifications, checks, replication, judgment, and accountability.

The verification frontier is the gap between producing a claim and justifiably accepting it. The claim may be true, useful, or neither; the frontier concerns whether the available evidence and review process warrant a decision. It is narrower than the whole safety problem and different from the compute frontier. It is also a working hypothesis, not a measured universal law. In some domains checking is cheap. In others, evidence production and independent review dominate the work. The practical question is where review capacity becomes the constraint as candidate generation grows.

This chapter joins ideas introduced earlier. Chapter 21 explained why checkable outcomes are powerful training signals. Chapter 27 treated verifiers as reasoning components. Chapter 52 required environment evidence instead of agent self-report. Chapter 55 examined protocols for systems that cannot be fully trusted. The missing bridge is an acceptance discipline: what is the claim, what evidence must accompany it, what do the checks establish, and who is authorized to decide?

A claim needs an evidence contract

The useful unit is a claim with evidence. Let $c$ denote the claim and $e$ its evidence bundle. A proof term, test report, execution trace, dataset, experimental protocol, model card, and record of objections can all be evidence. They are not equivalent evidence, and none accepts the claim by itself.

Before review begins, assign the claim to a class $j$: for example, a formal theorem, a software change, an empirical effect, or a release decision. Each claim class has a versioned evidence contract. One policy template is

$$A_j(c,e) = \mathbf{1}\!\left[ p_j(c,e)=1 \;\land\; \bigwedge_k h_{jk}(c,e)=1 \;\land\; \bigwedge_\ell s_{j\ell}(c,e) \geq \tau_{j\ell} \right].$$

Here $A_j(c,e)$ is the policy's binary acceptance output for claim class $j$; $p_j(c,e)$ is a provenance predicate; each $h_{jk}(c,e)$ is a required hard check indexed by $k$; each $s_{j\ell}(c,e)$ is a diagnostic score indexed by $\ell$; and $\tau_{j\ell}$ is that score's threshold. The symbol $\mathbf{1}[\cdot]$ returns one when every condition inside the brackets is true and zero otherwise; $\land$ means “and,” while $\bigwedge$ means that every indexed condition must hold.

This is a template for one versioned policy, not a universal definition of truth. The contract must say which hard checks and scores apply, what missing evidence does, and which acceptance authority owns the decision. A laboratory, maintainer, regulator, or incident commander may rationally reject a well-supported claim because risk or jurisdiction lies outside the formula. The equation makes a policy inspectable; it does not turn judgment into truth.

Verification capacity is a queue

Cost ratios hide the operational problem. A simple backlog makes it visible. For the same claim class and the same risk tier, $B_t$ denotes the number of items pending review at the start of interval $t$, $G_t$ denotes the new claims entering during that interval, and $R_t$ denotes the completed review decisions (accept, reject, or defer). Then

$$B_{t+1} = \max\{0, B_t + G_t - R_t\}.$$

The terms must use comparable units: a quick lint result and a clinical replication cannot share one queue. This equation is an accounting identity, not a queueing theorem. It omits priorities, variable service time, rework, and reviewer availability. It still exposes the governing fact: if arrivals exceed completed reviews for long enough, pending work accumulates.

def final_backlog(arrivals, reviews):
    backlog = 0
    for new_claims, completed_reviews in zip(arrivals, reviews):
        backlog = max(0, backlog + new_claims - completed_reviews)
    return backlog

intervals = 12
arrivals = [40] * intervals
fixed_reviews = [20] * intervals
scaled_reviews = [45] * intervals

print("fixed capacity backlog:", final_backlog(arrivals, fixed_reviews))
print("scaled capacity backlog:", final_backlog(arrivals, scaled_reviews))

The example is deliberately small. It does not predict a laboratory or product team. It shows why a generator benchmark is incomplete without an arrival rate, review capacity, time to decision, and age distribution for the backlog.

Different checks make different promises

“Verified” is useful only with an object and a guarantee attached. Each check answers a different question:

• Proof kernel. Establishes that a proof term derives an exact formal statement under the encoded axioms and kernel rules. It does not establish that the statement matches the intended claim or that the trusted computing base is flawless.
• Type checker, compiler proof, or static analysis. Establishes conformance to a stated type, translation, or program property. It does not establish every desired behavior of the program.
• Tests and execution. Establish behavior on the executed cases in the tested environment. They do not establish the absence of failures on untested inputs or environments.
• Simulator. Establishes behavior inside the simulator's model and assumptions. It does not establish the same behavior in the physical world.
• Computational reproduction. Establishes that a result can be regenerated with the same data, code, and methods. It does not establish replication with new data or freedom from shared bias.
• Empirical replication. Establishes that new data addressing the same question support a compatible result. It does not establish a timeless binary truth or suitability for every population.
• Model or human review. Produces a reasoned judgment under a rubric and the available evidence. It does not produce a certificate, and correlated review is not independent evidence.

The National Academies distinguishes reproducibility, which repeats a computation with the same data and methods, from replicability, which obtains consistent results with new data addressing the same scientific question (National Academies of Sciences, Engineering, and Medicine 2019). Replication is still a matter of degree, effect size, uncertainty, and scope. It is not an arrow that automatically changes “claim” into “fact.”

Formal proof as infrastructure

Formal mathematics makes the separation between proposal and acceptance unusually clear. A proof assistant needs a precise statement and a proof object. Its small kernel checks whether that object follows from the formal rules. The proof may be hard to find and cheap to check, but the guarantee ends at the formal boundary.

CompCert is a useful software example. Its verified back end establishes a specific semantic-preservation theorem for translation from Cminor to PowerPC assembly; it does not mean that an arbitrary compiler proves an arbitrary program correct (Leroy 2009). Flyspeck formalized the Kepler conjecture in HOL Light and Isabelle and produced machine-checked proofs of that formal statement (Hales et al. 2017). In both cases the evidence chain includes the statement, proof, kernel, libraries, and toolchain.

Neural theorem proving changes proof search, not this acceptance boundary. GPT-f generated Metamath proofs and found short proofs accepted into the library (Polu and Sutskever 2020). MiniF2F supplied 488 Olympiad-level formal statements, with complete Metamath and Lean translations and partial Isabelle and HOL Light coverage in its original release (Zheng et al. 2022). FrontierMath instead uses original expert-written problems and automated answer checks to reduce contamination; an answer checker is not the same thing as a formal proof of every solution (Glazer et al. 2024). On 12 June 2026, Epoch released FrontierMath v2 after correcting or removing issues that affected 42 percent of the problems; 338 remained. The checker could score an answer to the problem it was given, but it could not certify that the prompt and reference answer were sound (Epoch AI 2026). LeanDojo released tools, data, and benchmarks for reproducible Lean interaction and premise retrieval (Yang et al. 2023). DeepSeek-Prover-V2 combines informal decomposition with Lean 4 proof search (Ren et al. 2025), while AlphaGeometry2 combines a language model with a symbolic geometry engine (Chervonyi et al. 2025).

These systems narrow one part of the verification problem. Four gaps remain:

• Formalization gap. The exact formal statement must express the theorem people intend. A proof of the wrong formal statement can check perfectly.
• Library gap. Definitions, prior lemmas, and their assumptions are part of the evidence base.
• Kernel trust. The kernel is a small trusted computing base, not an infallible oracle; builds, hardware, and proof-export paths also matter.
• Translation gap. Natural-language discovery, informal argument, and formal proof are different artifacts. Connecting them is substantive work.

Discovery loops need evaluators

Automated discovery works especially well when candidates can be scored by code. AlphaEvolve searches over programs only after a human supplies evaluation code. That code maps candidates to scalar metrics, and therefore defines what improvement means. Tasks that require manual experimentation are outside the reported system's scope (Novikov et al. 2025).

This distinction prevents an attractive but dangerous shortcut. An evaluator score is search evidence, not an acceptance decision. In the reported applications, promising AlphaEvolve candidates passed checks appropriate to the case: held-out tests, expert checks, hardware validation, or post-deployment measurement. Its data-center scheduling result, for example, moved from simulation on historical snapshots to unseen workloads and then fleet measurement. The evaluation loop made search tractable; it did not abolish release review.

When the evaluator is a proxy, repeated optimization can exploit the difference between the metric and the intended goal. When it is a simulator, the result inherits the simulator's assumptions. When it is a learned judge, correlated errors can masquerade as confirmation. Discovery therefore needs a second boundary: validate the selected candidate with evidence that was not merely the fitness signal used to generate it.

When the verifier is weaker

The harder case is a claim whose evidence is complex and whose best available judge is weaker than the generator. Learned verifiers and scalable-oversight protocols try to increase review capacity, but none should be described as a proof system.

Process supervision is a scoped example. The PRM800K work collected roughly 800,000 human labels on steps in model-generated MATH solutions. A process reward model improved Best-of-N selection over the study's outcome-reward baseline; the experiment did not train the generator by reinforcement learning and did not show that every plausible chain of thought is faithful (Lightman et al. 2024). Generative verifiers train correctness as next-token prediction and can produce verification rationales, use chain-of-thought, and vote at inference time. Those rationales are learned judgments, not certificates (Zhang et al. 2025).

The broader protocols have similarly bounded evidence:

• Iterated amplification proposed recursive decomposition and tested five synthetic combinatorial tasks with a hard-coded decomposer. Those experiments did not establish that people can decompose difficult real-world judgments (Christiano et al. 2018).
• The original debate paper proposed adversarial argument under assumptions about optimal play; its experiment used MNIST and a sparse classifier rather than a human judge. It is a research program, not evidence that stronger systems will always expose one another's errors (Irving et al. 2018).
• Weak-to-strong experiments used GPT-family weak labels on NLP, chess, and reward modeling. Some methods recovered more capability than naive imitation, but remained below full strong-model supervision and did not simulate every property of human-to-superhuman oversight (Burns et al. 2024).
• AI control evaluated protocols on a sequence of 5,000 APPS programming tasks, with GPT-4 treated as untrusted, GPT-3.5 as trusted, and backdoored code built by red-team attack policies. The study demonstrates a control-evaluation method in that testbed, not a deployment guarantee for a genuinely misaligned system (Greenblatt et al. 2024).

The newest theoretical limit needs the same care. Friedl and colleagues model eliciting latent knowledge with a causal influence diagram. In their setup, the training distribution is a strict subset of possible cases, the evaluator is perfect on the training distribution but wrong somewhere off-distribution, and training can be indifferent between robustly capable agents. For this specified class of behavior-only feedback, training cannot guarantee an honest agent with certainty (Friedl et al. 2026). The theorem does not prove that every practical oversight method fails. It identifies assumptions under which behavior alone cannot rule out an evaluation-simulating solution.

Independence and provenance

Repeating one judgment is not the same as adding evidence. A generator, critic, and judge may share training data, architecture, retrieval sources, prompts, or organizational incentives. Their correlated agreement can be useful for search while remaining weak confirmation. Independence is therefore a property to document, not a synonym for “different model name.”

Provenance answers a second question: did reviewers check the artifact that was actually released? Preserve the candidate, configuration, data version, tool outputs, and evidence bundle by content hash. Record which checker version ran, who could change it, and which later transformation occurred. Without that link, an accepted proof, binary, dataset, or model can be silently replaced by an unchecked neighbor.

Failure modes

Several failures recur across domains:

• Proof by intimidation: length and technical fluency substitute for an accountable claim and check.
• Formalization error: the kernel proves a subtly different statement from the intended one.
• Coverage error: tests pass, but important inputs, environments, or properties were never exercised.
• Proxy capture: the generator learns to improve the evaluator without improving the real objective.
• Shared blind spots: apparently separate judges inherit the same failure.
• Unreproducible empiricism: code, data, and environment cannot regenerate the reported result.
• Acceptance laundering: “the model proposed” becomes “the institution knows” without an intervening evidence decision.

The countermeasure is not one universal verifier. It is a deliberately composed set of checks with explicit limits, followed by an accountable decision.

An operating ledger

For every consequential result, store a compact acceptance record:

1. Claim ID and class: the exact proposition, artifact, scope, and risk tier.
2. Evidence-contract version: required checks, thresholds, and deferral rule.
3. Generator and resource budget: model, prompt or scaffold, tools, attempts, compute, and elapsed time.
4. Evidence hash: immutable references to proofs, traces, code, data, and experimental protocols.
5. Checker versions and independence: tool versions, operators, data sources, conflicts, and shared dependencies.
6. Results and limits: hard-check outputs, diagnostic scores, uncertainty, failed checks, and unresolved objections.
7. Acceptance authority: named owner with the legal or operational mandate to decide.
8. Decision and date: accept, reject, or defer, with rationale.
9. Expiry condition: time, model change, evidence change, incident, or domain shift that forces review again.
10. Reproduction status: who reproduced the computation or replicated the empirical result, on which data and environment.

This ledger does not make weak evidence strong. It prevents uncertainty from disappearing as a claim moves from model output to report, product, or policy.

What this changes about the frontier

A model that proposes a theorem without a checkable proof has produced a lead, not an accepted theorem. A molecule with a promising simulated effect is a hypothesis, not a therapy. A migration plan that has not run against the target environment is a draft, not an operation. These are not semantic niceties; they identify the work that remains.

The frontier is an evidence-engineering problem. Measure the claim stream, the coverage and limits of each check, the review backlog, the time to decision, and the rate at which accepted claims later fail. Improving a generator without improving those systems may create value, noise, or both. The outcome depends on the domain and its acceptance machinery.

The handoff to the rest of the book is direct. Part XI asks how these constraints become markets, data rights, openness choices, and institutional incentives. Part XII asks how to operate systems under them: review gates, release evidence, SLOs, budgets, incident records, and operating contracts. Strong systems will not only generate useful candidates. They will make the path from claim to justified action explicit, inspectable, and proportionate to risk.

Further reading