AI Large-Scale Code Verification: A Practical Workflow

AI large-scale code verification starts with a requirement you can check, then combines behavior tests, security analysis and, where justified, formal specifications. The useful result is evidence about a particular revision and scope—not a blanket guarantee that an AI-written repository is correct.

Start with the runnable Python example, use the method selector to choose additional checks, then copy the verification record into your review.

Sources reviewed October 24, 2026. The Python fixture is an original teaching example. The external tools below are described from their documentation; this guide does not report a large-repository benchmark or an installation test of those tools.

Recent research: what Claude and Theorem verified

On October 22, 2026, Anthropic reported a collaboration with Theorem in which Claude generated Rocq proofs for 239 entry points across 123 OSS-Fuzz libraries. A proof checker evaluates the generated proofs against formal statements; a model's confident explanation is not the verification result.

The reported experiment targets compiled RISC-V binaries under a Linux process model, with single-threaded execution, static binaries, a fixed memory budget and inputs below 64 MB. The guarantee depends on the theorem, the modeled environment and trusted verification components. It does not establish that every library is free of every bug or that an arbitrary application can be proved with one prompt.

The public proof repository releases a subset and explains how to inspect statements and check proofs. Its coverage is narrower than the reported experiment: read the theorem for the particular binary and entry point you care about. We reviewed these sources; we did not reproduce the proofs.

For an application team, the practical starting point is still a precise claim and an observable check. The workflow below begins there and identifies when a stronger method is appropriate.

Choose the check for the claim

Compilation and type checking belong near the start: they can catch structural mistakes before more expensive checks run. They do not establish that the implementation meets the user's requirement.

Keep these checks complementary. Passing a security scan does not show that a CSV export preserves every record; passing an export test does not establish that its surrounding service enforces authorization.

Define a contract before asking an agent to verify code

For each change, identify:

• Revision and scope: the exact code, generated files and affected dependencies.
• Observable requirement: inputs, expected output and failure behavior.
• Important boundaries: empty input, duplicates, invalid values, state transitions or an authorization boundary where relevant.
• Independent expectation: a requirement, known fixture or trusted reference that does not merely repeat the new implementation.

If an agent writes both the implementation and its tests, review the expected behavior separately. Two artifacts can share the same misunderstanding. Ask for concrete evidence, not just a statement that the code was reviewed.

Run a small verification example

Suppose an AI-assisted change splits a list into batches. Its contract is: preserve every item in order, keep duplicates, leave the input unchanged, make every batch except the last full, and reject a non-positive size.

This example uses a finite list of integers and an integer size. It is a bounded teaching fixture, not a complete public-input validation library. Save the following as test_chunked.py in a disposable folder. It uses Python 3's standard library and does not call an AI service.

import unittest


def chunked(items, size):
    if size <= 0:
        raise ValueError("size must be positive")
    return [items[i:i + size] for i in range(0, len(items), size)]


class ChunkedTests(unittest.TestCase):
    def test_examples(self):
        cases = [
            ([], 3, []),
            ([4], 3, [[4]]),
            ([1, 2, 3, 4], 2, [[1, 2], [3, 4]]),
            ([1, 2, 3], 2, [[1, 2], [3]]),
            ([1, 1, 2], 2, [[1, 1], [2]]),
        ]
        for items, size, expected in cases:
            with self.subTest(items=items, size=size):
                self.assertEqual(chunked(items, size), expected)

    def test_bounded_properties(self):
        for length in range(9):
            for size in range(1, 5):
                with self.subTest(length=length, size=size):
                    items = [i % 3 for i in range(length)]
                    original = items.copy()
                    batches = chunked(items, size)
                    flattened = [item for batch in batches for item in batch]
                    self.assertEqual(flattened, original)
                    self.assertEqual(items, original)
                    self.assertTrue(all(1 <= len(b) <= size for b in batches))
                    self.assertTrue(all(len(b) == size for b in batches[:-1]))
                    self.assertEqual(len(batches), (length + size - 1) // size)

    def test_non_positive_size(self):
        for size in (0, -1):
            with self.subTest(size=size):
                with self.assertRaises(ValueError):
                    chunked([1], size)


if __name__ == "__main__":
    unittest.main()

From that folder, run:

python3 -m unittest -v test_chunked.py

A successful run reports three test methods as OK. They contain five explicit examples, 36 bounded property combinations and two invalid-size cases. That is evidence for this fixture's stated domain, not a claim about every Python value or your application.

Check that the suite can reject a plausible defect: in a disposable copy, change the loop's len(items) bound to len(items) - size. The tests should fail because full or trailing batches disappear. Restore the original bound before using the fixture. If the modified implementation still passes, inspect which file and tests actually ran.

For your own code, replace the function and expectations with your actual contract. Do not copy the batching properties onto an unrelated operation.

Add broader checks deliberately

Explore a larger input space with Hypothesis

Hypothesis's quickstart describes strategies and @given for generating test inputs. For the batching contract, a next step would generate lists containing duplicates and a range of positive batch sizes, then check the same order, preservation and sizing rules.

Choose realistic bounds, retain failing examples and make the expected properties reviewable. The fixed loops above are exhaustive only over their listed combinations; they are not a Hypothesis run. Neither approach proves correctness for all possible inputs.

Use CodeQL for supported security-analysis questions

GitHub's CodeQL overview explains analysis databases, queries and code-scanning alerts. Check the supported languages and framework models before selecting it for a repository.

Follow the documented setup appropriate to your account rather than assuming a generic scan covers every directory. GitHub's coverage troubleshooting guide explains how build-based analysis can omit files that were not built. Record omitted files and incomplete analysis alongside alerts.

A scan result is an input to review. Its absence of findings is not a proof that the application has no vulnerabilities.

Reserve formal verification for a specified claim

Dafny's tutorial explains preconditions, postconditions and the role of specifications. Its verifier checks Dafny code against those annotations. An incorrect or incomplete specification can establish the wrong property successfully.

For an existing Python or TypeScript service, this is not a command to prove the entire repository unchanged. Start with a critical algorithm or invariant you can model precisely, including any translation assumptions. Integration behavior and the surrounding system still need their own checks.

Scale the workflow across a repository

Use a small initial target, then extend the same evidence discipline to more packages. The following is a suggested rollout, not a benchmark or a ready-made CI configuration:

Do not make a diff-only check the sole basis for declaring a large system verified. Changes to a shared library, schema or generated interface may affect callers outside the edited files.

Track useful operational measures: regressions found, reproducibility of failures, elapsed verification time, and checks or paths skipped. A code-coverage percentage alone does not show that assertions express the right requirement.

Separate passed, failed, skipped, timed out and not analyzed. Give exceptions an owner and a review date. A failed or missing prerequisite cannot become a green result just because a later step produced no findings.

Copy a verification record

Use this original template in a change review or CI artifact:

Revision and requirement:
Languages, tool versions and relevant configuration:
Files/packages and affected consumers checked:
Commands, exit codes and evidence locations:
Expected behavior and tests actually executed:
Security-analysis coverage, query suite and findings:
Formal claim, assumptions and proof status, if applicable:
Skipped checks, timeouts and unexamined paths:
Exceptions, owner and next review date:
Decision and the precise scope that decision covers:

For the example above, the record should name the Python version, the saved file and the unittest command. It should also state that no integration, security scan or formal proof ran.

Check access, licenses and costs

GitHub's availability documentation distinguishes public-repository features from Code Security access for private or internal repositories. Confirm the relevant plan, product access and compute usage before enabling a workflow; this guide does not supply a universal free allowance or a fixed monthly price.

Dafny's source license is MIT. Hypothesis's repository license uses MPL 2.0 with stated exceptions for third-party material. Check the components and usage you actually choose. Software licensing, hosted features, compute and any connected AI model are separate considerations.

Frequently asked questions

Can one tool verify all AI-generated code?

Choose checks for specific claims and supported environments. The methods here provide different evidence; this guide has not established a universal verifier.

Why can green CI still miss a bug?

A requirement may be missing, an assertion may encode the wrong expectation, or an affected component may not have run. Inspect the checks and coverage that produced the green status.

Does a large repository always need formal verification?

Repository size alone is not the decision. Consider the consequence of a wrong result and whether a critical claim can be specified accurately enough to justify the proof work.

Is this the same as reverse engineering an application?

Reverse engineering investigates an existing artifact. Verification evaluates a stated claim about code or behavior. If artifact investigation is your starting point, see AI reverse-engineering tools and the REA overview, then define the requirement you want to check.