Empirical citations in this essay are graded. The 29 load-bearing claim groups (60 sub-items) were each challenged by 3 independent verifiers (word-for-word checks against primary sources, counter-evidence searches); all 29 survived refutation, 0 were overturned, and 40+ scope corrections from the verifiers are incorporated. Citations that did not enter the verification pipeline are marked 【unverified, source】. Vendor and interested-party numbers carry their measurement scope inline; a source index closes the essay.
This site's When Code Becomes Cheap concluded that AI pushes the software bottleneck to verification. AI Code Review asked whether an AI verifier can be trusted — the answer was conditional. A Foundation Inspection of Scalable Oversight dug to the bottom: "verification is easier than generation" stratifies by task family, and holds where an independent oracle exists. Together they leave one constructive question: in software, which judges depend on neither humans nor LLMs — and how much can LLMs scale each of them?
There is an authoritative map for this. Testing research calls the procedural criterion that distinguishes correct from incorrect behavior a test oracle; the survey by Barr, Harman, McMinn, Shahbaz & Yoo (IEEE TSE 2015) classified 694 publications (1978–2012) into four categories: specified oracles (mechanical judgment against a formal specification, 317 papers), derived oracles (judgment from derived artefacts — independent implementations, cross-execution relations, previous versions, 245), implicit oracles (general implicit knowledge — crashes and buffer overflows are nearly always errors, 76), and the case of no automated oracle, where humans judge (56). The same survey delivered a verdict: compared to other aspects of test automation, oracle automation "has received significantly less attention, and remains comparatively less well-solved" — a bottleneck that inhibits greater test automation. 【verified】
The bottleneck written down in 2015 is exactly where the industry aimed its LLMs after 2023. This essay audits that four-cell map cell by cell: who the judge is, how independent it is from LLMs, and whether the claimed LLM gains survive independent re-testing. Scope is strictly software/code oracles — not ML model evaluation.
Before the audit, fix the reading rules — otherwise this essay commits its own measurability bias, where gains appear everywhere because they are only visible where they are easy to measure.
First: who is the judge, and how far from the LLM? Proof checkers, compiler crashes, sanitizers, cross-implementation differencing, mutation gates, human triage — a spectrum from strongest independence to weakest. Second: what is this cell's own metric? Each cell's "LLM gain" must be scored by its own judge: independently confirmed coverage and vulnerabilities for fuzzing, verifier-judged proof completion for theorem proving, mutation-kill for tests, human-adjudicated true-positive rates for static analysis — numbers are not comparable across cells (different baselines, different denominators). Third: which seat does the LLM occupy? The same model can be a generator (producing test inputs), a proposer (drafting specs, rules, relations — filtered by an independent mechanism), or a judge (ruling directly). The spine claim of this essay is a falsifiable conditional: when the LLM sits in the generator or proposer seat and adjudication stays with an independent mechanism, gains come with hard numbers; when the LLM takes the judge's seat, claimed gains systematically shrink under independent re-testing. Counter-examples are reported in full, and the spine is softened accordingly at the end.
Two theorems verified in earlier essays are reused throughout: stronger models make increasingly similar errors (verified in AI Code Review, ICML 2025), which directly threatens every "LLMs cross-checking LLMs" judge; and an external sound verifier yields gains where self-critique collapses (verified in Scalable Oversight).
The cell with the strongest judge independence: Lean's kernel, SMT solvers, model checkers. Mechanical verdicts, unpersuadable, wrong is wrong.
On the completion-rate side, the numbers are genuinely hard. Goedel-Prover-V2-32B reaches 88.1% on miniF2F at pass@32, rising to 90.4% with two rounds of self-correction against Lean compiler errors — an increment that comes specifically from external verifier feedback, the direct quantification of "external sound verifier yields gains" in this cell. On PutnamBench it solves 86 problems (pass@184) with a model roughly 21× smaller than DeepSeek-Prover-V2-671B's 47 (pass@1024); its 8B variant beats the 671B model on miniF2F at the same pass@32, at roughly 80× smaller. 【verified】 AlphaProof used Lean verification results as grounded RL feedback to reach IMO 2024 silver-medal level (28/42, a combined score with AlphaGeometry 2; AlphaProof solved 3 problems alone, some taking 2–3 days, beyond contest limits — scope carried over, verified, from Scalable Oversight). The harder the judge, the more freely the model can grind — the cleanest positive cell in this essay.
But the attack surface has moved up one level: the verifier only guarantees proof ⊢ statement, never statement = intent. Four independent bodies of evidence draw the same crack:
assume(false), avalanching from one program to all programs, requiring an added critique layer (including an adversarial exploit model) to filter. What got hacked was not the sound verifier — it was the spec–implementation alignment layer. 【verified】The production-side contrast fixes our current position: in the AWS-led verification campaign for Rust's standard library (self-described as the largest reported library-verification campaign), the orders of magnitude came from deterministic tooling — Autoharness automatically produced 16,748 proof harnesses, 11,970 of which passed Kani verification; 989 functions in the whole campaign got verified formal contracts (295 automated + 694 from sixteen months of manual work) — while LLM contract synthesis carries the official verbatim label: "This approach is preliminary: the generated contracts require manual review before merging." 【verified】 A separate evaluation found that scoring specification autoformalization with an LLM-as-judge misses 26% of the failures caught by an executable evaluator 【unverified, source: arXiv 2605.26457】. In this cell, the LLM is already employable as a proposer — not yet qualified as a judge.
Crashes, memory violations, data races are "nearly always errors" — judges that need no specification and owe nothing to the artifact under test or its generator. This cell holds the hardest first-party numbers for LLM gains, and the most conspicuous empty square on the whole map.
OSS-Fuzz's two first-party reports are this cell's calibration data. August 2023: LLM-generated additional fuzz targets raised coverage on sample projects by 1.5%–31%, tinyxml2's line coverage from 38% to 69%, with no manual intervention. November 2024: AI-generated/enhanced targets covered 272 C/C++ projects, added 370K+ lines of coverage, and found 26 new vulnerabilities in projects already polished by hundreds of thousands of fuzzing hours (report-level scope: sanitizer crashes, human-reviewed, then reported to maintainers) — among them OpenSSL's CVE-2024-9143 (rated Low by OpenSSL), which by Google's own judgment had likely existed for about twenty years and was unreachable by existing human-written targets; reported 2024-09-16, fixed 10-16. 【verified】 Note who adjudicates along the chain: the LLM only writes targets; every verdict comes from ASan crashes and upstream fixes. On the same pipeline Google also tried LLM crash triage — and officially concedes that step is not yet trustworthy without human review. 【verified】
Big Sleep (Project Zero with DeepMind), in a variant-analysis setup seeded by recent commits, found an exploitable stack buffer underflow in SQLite's development branch — fixed the same day, intercepted before any official release. Two scope notes must travel with it: "the first public example of an AI agent finding a previously unknown exploitable memory-safety issue in widely used real-world software" is the team's self-assessment, promptly disputed by a researcher claiming an earlier case; and the team itself wrote that a target-specific traditional fuzzer would likely be at least as effective. 【verified】
Concurrency detectors: the only LLM-empty square among the eight cells this audit set out to cover. Traditional judges post hard production numbers here: Uber deployed race detection over 46 million lines of Go and in six months detected 2,000+ data races, fixing 1,000+ (PLDI 2022). 【verified】 The LLM has, to date, no first-party detection record "independently confirmed by TSan/KCSAN or upstream maintainers" (this investigation ran a systematic search; negative result). Its effective posture is in a different seat: Uber's Dr.Fix uses an LLM to draft fixes for 404 TSan-detected races — 224 (55%) successfully generated, of which 193 (86%) were accepted by developer review, behind a three-layer chain of "build + every test re-run 1,000× with no recurrence + human review." Worth recording: among the rejected 14%, some fixes passed the thousand-rerun gate and were still judged incorrect by humans — an independent machine gate is necessary, not sufficient. 【verified】 The empty square has a structural explanation: OSS-Fuzz's onboarding docs list only address/memory/undefined under sanitizers; ThreadSanitizer is de facto unplugged from the largest AI-fuzzing production pipeline (the infrastructure keeps a channel; a few Swift projects use it — not impossible, just not mainlined). 【verified】
This cell's judges come from derived artefacts: independent implementations checking each other (differential / pseudo-oracles) and cross-execution relations (metamorphic testing). It has the family's deepest war record — and one premise that the LLM era forces back into court.
Baselines first, gains second. Csmith (PLDI 2011) used randomized differential testing to report 325+ previously unknown C compiler bugs over three years (79 GCC, 202 LLVM, the rest commercial); 25 GCC bugs were flagged by developers at P1, the maximum release-blocking priority. The same paper's famous line: the middle-end wrong-code bugs found in every other compiler were absent from CompCert's verified portions — six CPU-years couldn't break it. 【verified】 SQLancer++ (ASPLOS 2026), using no LLM at all, reported 196 previously unknown bugs across 18 DBMSs (140 logic bugs), 92% already fixed. 【verified】 Every "LLM gain" must be compared against these baselines, not against a blank. This is not a hypothetical trap: Kitten (ISSTA 2025) — a simple mutation-based generator with no LLM — beat Fuzz4All's coverage by 48.3% (GCC) / 9.9% (LLVM) / 33.8% (Rustc) in 24-hour same-bench runs, finding 15–20 bugs per run where Fuzz4All found 5.7/0.3/0; part of the published "LLM gain" came from weak control groups. 【verified】
Csmith's authors named this cell's operating premise back in 2011: they never saw two unrelated compilers produce the same incorrect output on the same test case, crediting IR diversity — "if that did happen we would not detect that problem; this is an inherent limitation of differential testing without an oracle." The premise has been experimentally tested: Knight & Leveson 1986 had 27 teams independently implement one specification; across one million tests, coincident failures exceeded the independence assumption's prediction so far (z = 100.51) that the assumption was rejected at the 99% confidence level. 【verified】 The LLM-era replication arrived in 2026: 5 coding-agent systems × 23 models produced 48 versions; one million random tests observed 429 coincident failures against 115.36 predicted under independence (z = 29.20) — 3.7× the independence assumption, rejected again; yet three-version majority voting still cut mean failures from 387.44 to 130.99 (preprint). Voting judges over LLM panels: gains decay — they do not vanish. That is the spine's first softening clause. 【verified】
For the LLM's correct entry posture, this cell supplies the two cleanest controlled contrasts in the essay. One isolates the generator: ShQveL, on the same SQLancer++ chassis with the same TLP judge, swapped only the generator for GPT-4o-filled SQL fragments — 55 new unique bugs, 50 fixed 【verified】; in the same paper's controlled head-to-head, bare end-to-end LLM fuzzing (Fuzz4All with DuckDB docs) found 0 bugs in 6 hours at roughly 229× lower throughput — despite higher branch coverage (24.5% vs 21.3%); verbatim: "While exercising code is a necessary condition for finding a bug, it is not sufficient." 【verified】 The other swaps only the judge: Argus (SIGMOD 2026) has an LLM propose SQL-equivalent query-skeleton pairs, accepted as oracles only after the SQLSolver prover certifies equivalence — 41 previously unknown bugs across five heavily tested DBMSs, 36 confirmed, 27 fixed. In the ablation, replacing the prover with GPT-5 as judge, human adjudication found the 20 bug reports collected on DuckDB were all false positives (20/20), versus 0/20 for the prover-gated arm. The mechanism deserves verbatim memory: the LLM judge's per-pair error rate was only about 1/20, but true-bug base rates in mature DBMSs are so low that report-level false positives get amplified to 100% — low error rate × very low base rate = false alarms drowning true ones. 【verified】
The proposer seat for metamorphic relations behaves identically: unfiltered ChatGPT-proposed MRs, adjudicated by two domain experts (κ = 0.86), were correct at 49.3% for simple programs and just 7.0% for complex non-AI systems — even for the exhaustively studied sine function, 85% of candidates were wrong (preprint). SANER 2025's large-scale study (37 systems under test) found only 29.86%/43.79% of GPT-3.5/GPT-4-proposed MRs valid — yet 38.63% of GPT-4's candidates were genuinely novel MRs never identified before. 【verified】 The proposing talent is real; so is the >50% invalidity: output must pass an independent filter — only then is it an asset. Plugged into a hard judge, LLM generators have reached the deepest bug stratum: LegoFuzz wired LLM-generated code blocks into cross-compiler checksum differencing, reporting 66 GCC/LLVM bugs, 30 of them miscompilations 【unverified, source: arXiv 2508.18955】; by contrast its authors' literature-level audit of public reports concluded Fuzz4All and WhiteFox found not a single miscompilation — Fuzz4All's oracle is crash/assertion by construction and cannot see silent wrong-code; undifferentiated "confirmed bug counts" overstate reach. 【verified】
In property-based testing and invariant mining the judge is the property itself: once written, adjudication is mechanical — but who holds the power to define the property decides this cell's grade. Forty years ago Daikon honestly called its own output likely invariants — properties observed from the implementation itself; if the program is wrong, the oracle is wrong with it 【unverified, source: Ernst et al., SCP 2007】. LLM-drafted properties are the same structural weakness, amplified.
The sub-cell where the judge is an SMT solver/verifier has the hardest numbers. LaM4Inv (ASE 2024) — "LLM guesses predicates + BMC falsification filter + SMT final ruling" — solved 309 of 316 C programs (97.8%) against the strongest prior baseline G-CLN's 219 and RL-based Code2Inv's 210, averaging just 3.7 query rounds per problem; Microsoft's Loopy (GPT-4 + Frama-C adjudication) solved 398/469, still fewer than the symbolic tool Ultimate Automizer's 430, but including 31 problems the latter fails — with the bulk of its gain coming from the non-LLM Houdini filter (293→383). 【verified】 Then the cold water: InvBench (2025, v1) re-tested under the net-contribution metric of "speeding up a SOTA verifier": the strongest model, o3, achieved speedups on only 28.3% of the easy split, averaging 1.09×, with negligible gains on the hard split — "correct invariants" are an order of magnitude short of "useful" (note the benchmark's January 2026 v2, renamed Quokka, reports positive results — yet instances achieving ≥1.2× speedup remain under one in ten). 【verified】
In the sub-cell where LLMs draft properties freely, the attenuation layer is cleanly measurable. Manual annotation of 219 LLM-generated PBT properties found 21% unsound (two annotators, κ = 0.862), rooted in property hallucination and boundary slips; under a mutation gate, the strongest model, GPT-4, could synthesize correct PBTs for only 21% of documentation-extractable properties. 【verified】 nl2postcond (FSE 2024) classified finer: 47.4% of LLM postconditions contain type-check components (pure type checks alone: 16%), with bug-completeness of just 0.14 for that class; on real Defects4J, all models and prompts combined discriminated only 64/525 bugs (12.2%) — per-property "correctness" runs high, while "lethality" sits behind a whole layer of trivial-property decay. 【verified】 A controlled study further found LLM-generated oracles systematically capture actual implementation behavior rather than expected behavior, with below-50% accuracy at judging oracle correctness 【unverified, source: arXiv 2410.21136】.
That the evaluation protocol of learned oracles is itself a systemic risk has a pre-LLM smoking gun. TOGA (ICSE 2022) once claimed 57 bugs found on Defects4J, 30 exclusively; two independent re-tests arrived: ESEC/FSE 2023, over 25 real systems and 51K injected faults, measured 47%+ of its assertions as false positives, with true-positive assertions adding just 0.3% fault-detection; ISSTA 2023, after fixing an evaluation leak ("test prefixes taken from the fixed version," which inflated bug counts by 61.8%), measured precision at 0.38% — a zero-information baseline of "expect no exception" found 61% of its bugs at twice the precision. 【verified】 Model defines its own judge → independent re-test → gain shrinks from "30 exclusive bugs" to 0.3% — the spine's most complete materialization.
The counter-example line, recorded in full: Anthropic's Agentic PBT (Claude Opus 4.1 + Hypothesis) swept 100 Python packages and produced 984 bug reports; the authors randomly sampled 50 from the top-80%-scored reports for independent review, judging 56.0% real bugs (95% CI 42.2–69.8%) and 32.0% worth reporting; 5 were actually reported, and 3 patches were merged upstream into NumPy and others. Three scope notes: the sample excludes the lowest-scored fifth of reports, the confidence intervals are wide, and the authors are both the vendor (evaluating their own model) and — in one case — a core maintainer of Hypothesis itself. The bugs are real, but this is the record of a full chain — "LLM proposes + pytest executes + human review + maintainer final ruling" — not of an LLM judge. 【verified】
Tests are the most widespread oracle — but who judges the tests? Mutation testing's answer: inject small faults and see whether the exam kills them. In 1978, DeMillo, Lipton & Sayward wrote down its two assumptions (competent programmer and the coupling effect), honestly declaring the latter beyond proof, an empirical principle 【unverified, source: IEEE Computer 1978 PDF】. This cell's modern question: once LLMs mass-produce tests, what gate stops things that merely look like tests?
Meta supplied two production-grade answers — every number below cited post-correction. TestGen-LLM (FSE 2024), behind three independent gates: in the Instagram Reels/Stories evaluation (86 Kotlin components), 75% of test classes had at least one generated case that built, 57% at least one that passed stably 5 consecutive runs, 25% at least one that genuinely increased line coverage — note the denominator is test classes under an "at least one" scope, not "75% of generated cases compiled"; overall, 73% of improvement recommendations were accepted by engineers (a merged figure across events; per-event acceptance ranged roughly 51%–94%). ACH (FSE 2025) industrialized the mutation gate itself: over 10,795 Kotlin classes on 7 platforms it generated 31,677 mutants, 29% (9,095) surviving the "compiles and isn't killed by existing tests" filter, yielding 571 privacy-hardening tests, with 73% test-a-thon acceptance. 【verified】 Same structure throughout: the LLM sits in the generator seat; build/execution/coverage/mutation gates run the machinery; humans keep the final ruling.
Independent academia marked two calibration lines for this cell. First, which direction contamination pushes: on the uncontaminated ULT benchmark, 12 open-source LLMs (1.3B–33B) saw statement coverage halve from 92.18% on the old benchmark to 45.10%, while mutation score fell from 49.69% to 40.21%; a controlled contrast showed test leakage alone lifts coverage and kill rates by about 10 points each — coverage saturates easily on simple benchmarks and inflates more, so evaluations reporting coverage without lethality get discounted first (ACM TOSEM; note: no frontier closed models included). 【verified】 Second, what assertions actually anchor to: across 22,374 program variants, even when tests were regenerated by the LLM looking at the modified code, 99% of the 23,977 tests failing on the new code passed on the original program while executing the modified region — the paper names it residual alignment: the LLM does not derive assertions from the code in front of it, but recalls the standard algorithm's behavior from training memory, even treating the modified code as a "buggy version of the original." 【verified】 Assertions anchor to training priors, not the implementation under test — which is why they naturally suit the regression gate (locking in the status quo) and not the correctness judge. The ceiling for proactively catching unknown bugs has also been measured: TestExplora, on 2,389 real tasks with every defect signal hidden, found the strongest tested models reach a maximum single-shot Fail-to-Pass rate of 16.06%, with agentic setups at 29.7% over five attempts (as of the models/agents tested). 【verified】
A static-analysis rule is a specification the analyzer executes mechanically — but its false positives are adjudicated by humans, so the cell is born half machine, half human.
LLM as proposer: real gains on the recall side. IRIS (ICLR 2025) has the LLM infer taint source/sink specifications, executed independently by CodeQL's dataflow engine: on 120 manually validated real Java vulnerabilities it detected 55, more than doubling CodeQL's official queries at 27, and found 4 unknown vulnerabilities in the latest versions of 30 projects that existing tools miss. The fine print must travel in the same sentence: its average false discovery rate remains 84.82% under the paper's scope (self-described as a conservative upper bound; a manual-sample refined estimate is ~46%) — even optimistically, nearly half of all reports still need human ruling. The LLM lifted recall; the precision floor didn't move. 【verified】
LLM as bare detector: the steepest shrink curve in this essay. PrimeVul (ICSE 2025): a SOTA 7B model scores 68.26% F1 on the old BigVul benchmark and 3.09% on PrimeVul — de-leaked, time-split, labels spot-checked by humans — a ~22× shrink; GPT-3.5/GPT-4, under the strictest vulnerable-vs-patched paired evaluation, perform "no better than a random guess." SecLLMHolmes (IEEE S&P 2024) adds the robustness check: merely renaming functions/variables flips GPT-4's verdicts in 17% of cases. 【verified】 A judge whose rulings don't rest on program semantics has no business on the bench.
The triage seat is the spine's textbook case. Semgrep's official blog headline: "Assistant agrees with researchers 96% of the time." The fine print: final agreement on the false-positive side is just 41% (25% early in the project, ~55% overall), and the company concedes the design is deliberately conservative — more likely to suggest fixing a false positive than to ignore a true one. A noise-reduction tool's value lies precisely on the false-positive side — where the LLM judge fails. On the independent SastBench (2,737 alerts, 299 real CVEs), the best agentic LLM triage configuration manages 16.9% precision, MCC 0.148 (different distribution from vendor headlines, no same-bench division — but the magnitude gap stands). 【verified】 A narrow-domain counter-example exists: Tencent eliminated 94–98% of false positives on 3 bug classes using LLM + static hybrid evidence 【unverified, source: industrial paper, research notes】 — the triage seat isn't unsittable; it's sittable only in narrow domains with an independent evidence source underneath.
Barr's fourth cell is "no automated oracle — humans judge." Across 2024–2026 this cell staged the cleanest natural experiment on the map: the same LLM-produced "security findings," with or without an independent judge, ended in opposite fates.
Act one: the flood. curl maintainer Daniel Stenberg's first-party numbers from July 2025: about 20% of security submissions judged AI slop, only ~5% ultimately real vulnerabilities; each report consumes 3–4 people at half an hour to three hours each, on a team of 7. In January 2026 curl closed its seven-year bug bounty (87 confirmed vulnerabilities, $100K+ paid out): confirmation rates had collapsed from a historical >15% to <5% in 2025. The Linux kernel security list rose from ~2–3 reports/week two years prior to ~10/week in 2025, the increase being "only AI slop"; the Python ecosystem's triagers independently reported the same phenomenon 【unverified, source: sethmlarson.dev, 2024-12】. Mozilla, meanwhile, self-reported no significant increase in AI low-quality reports (five or six rejections a month, under 10% of the total) 【unverified, source: TechCrunch quoting a spokesperson, 2025-07】 — the flood is real but uneven, modulated by bounty incentives and reporting friction.
Act two: the reversal. After curl returned to HackerOne in March 2026, report frequency roughly doubled versus 2025 while the confirmation rate recovered and overshot to 15–16%; Stenberg wrote that "Almost every security report now uses AI to various degrees." The kernel matched: from early 2026, 5–10 reports a day, mostly correct — so much so that Torvalds declared in the 7.1-rc4 announcement that the private security list had become "almost entirely unmanageable," the main cause being mass duplication from different people running the same tools; the failure mode had flipped from "fake reports" to "correct but duplicated." The new kernel policy (drafted by Tarreau) classifies AI-assisted findings as public disclosure, requires a tested reproducer, and urges an accompanying patch — Torvalds verbatim: "If you actually want to add value, read the documentation, create a patch too." 【verified】
Read the mechanism in full: one and the same underlying capability, plugged into a sanitizer crash gate, yields 26 vulnerabilities and a twenty-year CVE; dumped onto a human triage desk in 2025, it yields a slop flood costing a 7-person team a dozen person-hours a week. The judge's independence and mechanicality decide whether the same LLM output is an asset or a burden. But act two is the spine's second softening clause: the human-judge cell's output quality is a function of incentive structure × tool generation, not a permanent law — and the kernel's remedy vindicates this essay's frame: push the burden of proof back to the submitter and demand machine-verifiable artifacts (reproducers, patches).
Scalable Oversight already built this cell's frame: production is the most independent, unpersuadable judge, but it rules after the fact, its verdict costs the blast radius, and "ran fine so far" is not an acquittal. What this essay adds is the AI-coding-era evidence — whose very shape is the finding: this cell has no clean numbers; claims in both directions are soft.
The negative direction: DORA 2024 reported AI adoption associated with delivery throughput −1.5% and delivery stability −7.2%, with 2025 seeing throughput turn positive while stability stayed negative for a second consecutive year (observational survey scope; carried over, verified, from When Code Becomes Cheap); Georgia Tech's AI-attributed CVE tracker confirmed a cumulative 74 in Q1 2026, self-described as a floor (attribution via Git history of fixing commits; verdicts lag by months) 【unverified, source: CSA research note 2026】. But symmetry must be paid in full: vendors' negative numbers also fail independent re-testing — GitClear's "rising churn" narrative was contradicted head-on by a longitudinal analysis of 151 self-admitted GenAI-using open-source repositories (no general churn increase, "contradicting popular narratives") 【unverified, source: arXiv 2507.10422】. The cell's one first-party hard point for LLM gains runs in a single direction: reducing LLM output to independently checkable representations — Microsoft's Argos has the LLM generate explainable, reproducible anomaly-detection rules for runtime monitoring, with F1 up to +28.3% on labeled datasets including production telemetry 【unverified, source: arXiv 2501.14170】. Once the rule is written down, adjudication no longer depends on the LLM — the seat theory again.
Spread the nine cells out and the spine claim holds as a conditional — more precise than the pre-registration: what decides whether an "LLM gain" is real is not the cell, but the seat the LLM occupies in the verification chain:
Three softening clauses, lest the conditional get axiomatized like its predecessor: voting judges over LLM panels decay, they don't zero out (387→131); the human-judge flood is incentive-modulated and reversible across tool generations (curl's 15–16% overshoot); independent machine gates are necessary, not sufficient (Dr.Fix's thousand-rerun survivors still 14% human-rejected). Plus one cross-cell rule: gains must be measured against strong non-LLM baselines (Kitten, SQLancer++, AWS Autoharness) — gains measured against blanks evaporate first under re-testing.
Scalable Oversight concluded that "verification is easier than generation" stratifies by oracle independence; this essay supplies its constructive face: software happens to be one of the few human domains equipped with a whole cabinet of independent mechanical judges — proof checkers, sanitizers, differencing, mutation gates. The core of LLM-era verification engineering is not building a smarter judge, but wiring the LLM's unbounded capacity to these unpersuadable ones — and never forgetting which seat it must not take.
Ordered by evidence strength:
Signals worth watching: whether OSS-Fuzz plugging in TSan lets LLM-generated targets replicate the memory-safety record in the concurrency cell; whether Quokka's (né InvBench) positive re-report survives third-party replication; whether the kernel's "attach a patch" rule tames the duplication flood within a year of machine-verifiable artifacts; and the next TOGA-shaped case — which "LLM judge" product will first publish false-positive-side numbers with independent re-testing.
Taxonomy & founding literature: Barr, Harman, McMinn, Shahbaz & Yoo, "The Oracle Problem in Software Testing: A Survey" (IEEE TSE 41(5), 2015) · Weyuker, "On Testing Non-testable Programs" (1982) · McKeeman, differential testing (1998) · Chen, Cheung & Yiu, metamorphic testing (HKUST-CS98-01) · DeMillo, Lipton & Sayward (IEEE Computer 1978) · Claessen & Hughes, QuickCheck (ICFP 2000) · Ernst et al., Daikon (SCP 2007) · Newcombe et al., "How AWS Uses Formal Methods" (CACM 2015, carried from #0) · Knight & Leveson (IEEE TSE 1986) · Yang, Chen, Eide & Regehr, Csmith (PLDI 2011)
Formal-verification cell: Goedel-Prover-V2 (arXiv 2508.03613) · AlphaProof (Nature 2025, carried from #3) · miniF2F-Lean Revisited (arXiv 2511.03108, NeurIPS 2025) · ReForm (arXiv 2510.24592) · NL→TLA+ evaluation (arXiv 2606.05792, ICSOFT 2026) · AlphaVerus (arXiv 2412.06176) · Verifying the Rust Standard Library (arXiv 2606.17374) · Verus-SpecGym (arXiv 2605.26457)
Fuzzing & concurrency cells: Google Security Blog, "AI-Powered Fuzzing" (2023-08) and "Leveling Up Fuzzing" (2024-11) · Project Zero, "From Naptime to Big Sleep" (2024-11) · Chabbi & Ramanathan, Uber Go races (PLDI 2022) · Behrang et al., Dr.Fix (PLDI 2025) · OSS-Fuzz new project guide · SC-W 2023 LLM race detection (arXiv 2308.07505)
Differencing/metamorphic cell: SQLancer++ (arXiv 2503.21424, ASPLOS 2026) · ShQveL (arXiv 2505.02012) · Argus (arXiv 2510.06663, SIGMOD 2026) · Fuzz4All (ICSE 2024) · Kitten (ISSTA 2025) · LegoFuzz (arXiv 2508.18955) · Luu, Liu & Chen, ChatGPT MRs (arXiv 2310.19204) · Zhang et al., SANER 2025 · "N-Version Programming with Coding Agents" (arXiv 2606.20158)
PBT/invariants cell: Vikram et al. (arXiv 2307.04346) · Endres et al., nl2postcond (FSE 2024) · LaM4Inv (ASE 2024) · Loopy (arXiv 2311.07948) · InvBench/Quokka (arXiv 2509.21629 v1/v2) · TOGA re-tests: Hossain et al. (ESEC/FSE 2023) and Zhongxin Liu, Kui Liu et al. (ISSTA 2023) · Konstantinou et al. (arXiv 2410.21136) · Anthropic Agentic PBT (arXiv 2510.09907)
Testing/mutation cell: Alshahwan et al., TestGen-LLM (FSE 2024) · Foster et al., ACH (FSE 2025) · ULT/UnLeakedTestbench (ACM TOSEM, arXiv 2508.00408) · LLM tests under software evolution (arXiv 2603.23443) · TestExplora (arXiv 2602.10471)
Static-analysis cell: IRIS (ICLR 2025) · PrimeVul (ICSE 2025) · SecLLMHolmes (IEEE S&P 2024) · Semgrep official blog (2025) · SastBench (arXiv 2601.02941)
Human-judge cell: Stenberg, "death by a thousand slops" (2025-07) / "The end of the curl bug-bounty" (2026-01) / "High-Quality Chaos" (2026-04) · Tarreau, LWN (2026-03) · Torvalds, LKML 7.1-rc4 (2026-05) · Larson, sethmlarson.dev (2024-12) · TechCrunch (2025-07)
Production cell: DORA 2024/2025 (carried from #0) · CSA/Georgia Tech AI-CVE tracker (2026) · Ebert et al. (arXiv 2507.10422) · Argos (arXiv 2501.14170) · Goel et al., error convergence (ICML 2025, carried from #2)
Research materials and all verification rulings are archived in the research base (8+3 investigation lines, 208 claims, 29 load-bearing groups × 3 votes, all 87 votes on record).