Verifying AI-Generated Code

Review AI-generated code by distinguishing what compilation and tests establish, then matching review effort to the impact of the change.

Why verification became the new bottleneck

Faster code generation does not reduce total development time by the same proportion. Developers still need to understand the result and compare it with the requirements.

In Stack Overflow's 2025 developer survey, 84% of respondents said they use AI tools or plan to use them. In the accuracy question, 33% reported trust, with high trust accounting for 3% of all responses. Adoption intent and confidence in the results remain far apart.

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 described the accumulation of unchecked code as verification debt. Deferring review can force later changes to revisit earlier assumptions, so generated volume and verification capacity need to be managed together.

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.

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 code and tests can make them share 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

This article groups verification into syntax, behavior, semantics, and formal proof. Their questions overlap, but passing one type of check does not establish that all requirements have been verified.

Syntax and behavior are easier to automate, but a passing result covers only what each tool checked. Formal verification does not finish automatically once a specification exists; users may need to supply loop invariants and supporting lemmas. Verification design decides which tools cover each axis and how far that coverage extends.

From deterministic checks to formal verification

The following is an example of connecting the four axes from generation through operations. Cheap, fast filters come first, and expensive verification is pushed back.

The L1 deterministic layer is a low-cost first filter. Compilers and type checkers catch syntax and type errors, but they cannot establish that compiling code has the intended meaning. Teams can make static analysis tools such as ESLint, Semgrep, and CodeQL blocking checks for AI changes. An abstract syntax tree (AST) check can also extract called identifiers and compare them with the library's real API.

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 asks another LLM to grade the code. A model that writes and grades the same change may share blind spots across both passes. For changes that need stronger independence, a policy can require a different model or an external oracle before auto-merge.

The L4 formal verification layer proves properties stated in a specification. Dafny and Verus provide SMT-backed automation, while Lean is an interactive theorem prover in which users construct proof obligations and tactics. When automation stalls, developers may need loop invariants or supporting lemmas, so the practical scope starts with modules whose failures are costly.

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.

The table below is an example review policy. Adjust reviewer counts and change-size thresholds to the organization's risk tolerance.

Apply automatic merging only to changes that pass required CI and review conditions. Model reviews and static analysis can be part of the chosen policy, but different models can still miss the same error. Policy engines and repository merge rules can enforce the selected conditions.

Code that clears the gate is still not finished. The deployment guard (L6) can, for example, ramp 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-generated code starts by distinguishing the scope of syntax, behavior, semantics, and formal checks. Fast automated checks can filter changes before execution tests and review focus on those with greater impact. Independent criteria help prevent code and tests from sharing the same incorrect assumptions. Track errors after deployment and use missed conditions to improve subsequent checks.