Verifying AI-Generated Code

AI produces code at machine speed, but confirming that the code is correct is still bound to human speed. This covers the multi-layer verification structure that fills the gap.

Why verification became the new bottleneck

As generation got faster, the bottleneck in development moved from writing to verifying. More time now goes into deciding whether the output is right than into typing it.

In the Stack Overflow developer survey published in 2025, over 84% of respondents said they use AI tools. Only 29%, however, said they fully trust the output. The tools spread, but trust did not follow.

Productivity numbers do not all point one way either. A randomized controlled trial (RCT) published by METR in July 2025 found the opposite result: experienced open source developers were 19% slower when using AI. The interpretation is that faster writing was eaten by the review and correction that followed.

AWS chief technology officer (CTO) Werner Vogels called this phenomenon verification debt. Code piles up at machine speed while confirming its correctness stays bound to human speed, and the difference accumulates as invisible debt. Defects do not surface immediately, so the debt builds and then breaks all at once, and it accumulates faster than AI pays it down.

Code that compiles and is still wrong

The awkward property of AI code is that it is assembled plausibly. It compiles and passes basic unit tests, but neither guarantees it does what was intended. The distinction is between being plausible by construction and being correct by construction.

Empirical numbers back up the gap.

The conclusion these numbers point to is clear. Problems in AI code stay around a long time if they are not caught early, and no single check filters them out.

There is one more trap here. Asking the same model for both the code and the tests makes the two share the same blind spots. If the code rests on a wrong assumption, the tests rest on that same assumption and pass it. This is called the tautological test trap.

The four axes of verification

Regardless of how autonomous the process is, every verification activity sits on one of four axes. Each axis asks a different question, so clearing one leaves the others entirely empty.

The easy axes to automate are syntax and behavior. The semantic axis requires knowing intent, so it stays partially automated, and the formal axis becomes fully automatic only when a specification exists. Designing a verification process comes down to deciding which tools cover which of these four axes, and how far.

From deterministic checks to formal verification

In practice the four axes unfold into layers that run from generation through operations. Cheap, fast filters come first, and expensive verification is pushed back.

The L1 deterministic layer is a near-free first filter. Compilers and type checkers catch code that compiles but is semantically wrong. Running static application security testing (SAST) tools such as ESLint, Semgrep, and CodeQL as blocking checks on every AI commit is the 2026 standard. Adding abstract syntax tree (AST) cross-checking on top also catches hallucinated calls. The check parses the AST of the generated code and compares the API signatures it uses against the library sources.

The L2 execution layer covers what can only be learned by running the code. The core techniques are as follows.

• Property-based testing (PBT): repeatedly checks invariants such as "the result is non-negative for every input" against randomized inputs.
• Differential testing: feeds the same input to the existing implementation and the AI implementation and compares outputs. This is central to migrations and refactors.
• Fuzzers (libFuzzer, AFL++) and sandboxes: treat AI code as adversarial and run it in an isolated environment with the network cut off.

JiTTests (Just-in-Time Tests), released by Meta in February 2026, generates tests on the spot for the specific changed diff. Meta reported that it caught roughly 4x more regressions than their existing hardening tests (per Meta's announcement).

Differential testing verifies code without writing out expected answers one by one, because the existing implementation serves as the oracle and only output equality matters. Below is a minimal example built from the standard library alone, which passes 20,000 inputs.

import random
 
# under verification: the new implementation written by AI
def new_impl(xs):
    return sum(x for x in xs if x > 0)
 
# oracle: the existing, trusted implementation
def old_impl(xs):
    total = 0
    for x in xs:
        if x > 0:
            total += x
    return total
 
def test_differential_and_property():
    rng = random.Random(0)
    for _ in range(20000):
        xs = [rng.randint(-50, 50) for _ in range(rng.randint(0, 20))]
        assert new_impl(xs) == old_impl(xs)   # differential: do the two agree
        assert new_impl(xs) >= 0              # property: always non-negative
 
if __name__ == "__main__":
    test_differential_and_property()
    print("OK")

The L3 LLM judging layer is the LLM-as-Judge approach, where another LLM grades the code. If the model that wrote the code is the same one grading it, the tautological trap applies. That is why auto-merge policies frequently require approval from a model built by a different vendor.

The L4 formal verification layer proves specification compliance mathematically. Specifications written in Dafny, Lean, or Verus are discharged by an SMT solver in the background. The cost is high, so applying it only to safety-critical modules such as aerospace, medical, financial cores, and autonomous driving is the realistic approach.

Where humans remain

No amount of automated verification removes people entirely. According to the Macroscope 2025 benchmark, even leading AI review tools catch only about 50% of real bugs. The human gate (L5) therefore scales review intensity with the blast radius of a change, meaning how far the damage spreads when something goes wrong.

Even where auto-merge is allowed, the conditions are strict. Every CI check must pass, and a model from a different vendor must have judged the change. Diff coverage plus CodeQL and Snyk must be satisfied, and the diff size must stay under a cap. Engines such as Mergify, Kodiak, and OPA enforce that policy.

Code that clears the gate is still not finished. The deployment guard (L6) ramps canary traffic up from 1% and rolls back automatically once the error rate crosses a threshold. Production monitoring (L7) tracks change failure rate and mean time to recovery (MTTR), managing the survival rate of AI-introduced issues as a separate metric.

Summary

Verifying AI-written code is not a single technique; it has settled into a layered defense running from generation through CI, deployment, and operations. The four axes of syntax, behavior, semantics, and formal proof unfold into layers. Those layers are deterministic, execution, LLM judging, formal verification, human gate, deployment guard, and monitoring. Putting cheap checks first and deferring expensive ones is the standard ordering.

Handing both code and tests to the same model makes them share blind spots. Mechanisms such as an external oracle in differential testing or grading by a model from a different vendor matter. What it comes down to is tuning the balance of automation and human review to the blast radius of each change. Teams also have to keep measuring the survival rate of AI-introduced issues after deployment.