AI-Generated Formal Proofs at Scale: The Shift in Software Security Verification

1. A Set of Numbers Worth Noting

A recently disclosed effort, jointly published by an AI research team and a team focused on formal methods, has generated a fair amount of discussion in the software security community. The headline figures are roughly:

• Scope: 123 open-source code repositories, 239 test entry points
• Output volume: about 180 million lines of formal proof (machine-checkable)
• Unexpected yield: hundreds of real defects, some of which reportedly evaded random test inputs on the order of trillions of executions and had been latent for years
• Verification level: assembly / machine code, not source level
• Time cost: weeks, where comparable work has historically required expert effort on the order of a dozen person-years

Taken at face value, it is easy to conclude that “AI writes proofs now, so human verification is out of a job.” That conclusion is both incomplete and inaccurate. The more interesting question is what the work actually changes: the input-cost structure of formal verification.

2. Sampling vs. Exhaustion: Two Fundamentally Different Ways to Find Bugs

In engineering practice there are two main routes to finding defects. They are not a new method replacing an old one; they answer two different questions.

Fuzzing (random or structure-aware input generation) constructs large volumes of inputs and hammers the program with them, watching for crashes, hangs, memory errors, or undefined behavior. It is highly industrialized, has a low false-positive rate, parallelizes well, and is standard infrastructure in continuous integration. But it has two structural limits:

1. It only covers the input space that was sampled. If the millionth input was fine, the million-and-first may not be. Its conclusion is always “everything I tried was fine.”
2. It depends on an oracle. Deciding whether an execution counts as wrong requires a decidable criterion — a process crash, a timeout, an out-of-bounds memory access report. Semantic errors outside those criteria (a decryption result that is simply incorrect but does not crash) are structurally invisible to it.

Formal verification takes a different route entirely: it states “the program cannot trigger this class of error on any input” as a mathematical proposition, then derives it step by step under strict rules until it reaches a machine-checkable, complete proof. The conclusion is not a sampling statistic but an exhaustive claim over all inputs, under a given model.

An architectural analogy is more precise than the one usually offered: fuzzing is sending people into a building to jump around and see where it collapses. Formal verification is not “reading the blueprints” — it is a complete solve of the structural mechanics equations, with a solution process a third party can re-check step by step. The cost is that the equations only cover what you put into the model: material parameters, load assumptions, boundary conditions. Whatever is left out is not covered by the conclusion. This point recurs in the risk section below.

3. Why Formal Verification Has Long Been “Too Expensive to Use”

Cost is not simply “writing proofs is tedious.” Broken down, there are four real sources:

1. Cost of stating the proposition. The first step is translating a security intent into a precise, unambiguous mathematical statement. This step is nearly impossible to automate and depends heavily on domain experts.
2. Cost of discovering invariants and auxiliary lemmas. Correctness for recursive data structures, loops, and concurrent interleavings often hinges on one critical invariant, and finding it is usually the hardest part.
3. Cost of solving and iterating. Automated solvers time out on complex theories, requiring humans to split problems, reformulate representations, and supply hints — a long human-in-the-loop cycle of tool dialogue.
4. Maintenance cost. Change the code and proofs may fail wholesale, so re-verification is another full round of investment.

One figure often cited in industry: in a well-known high-assurance microkernel case, verification effort was on the order of ten times the effort of writing equivalent code. Because of that cost curve, high-assurance verification has for decades concentrated on code that is “fatal if wrong and slow to change” — avionics, orbital control, automotive functional safety. For the vast majority of business systems, the marginal cost of verification far exceeds the benefit, so the default route has necessarily been testing plus code review.

4. What Changed This Time: Propositions Come for Free

The clever part of this work is not that the model learned to write proofs. It is that it eliminates item 1 above.

Public continuous-fuzzing platforms have accumulated, over a long period, a large body of test entry points written for open-source projects — the functions or components that get hammered repeatedly. Each entry point carries an implicit but precise semantics:

The entry point returns normally for any input = no defect triggered; the entry point crashes or goes out of bounds = a defect exists.

In other words, “this entry point is safe for arbitrary inputs” is already a ready-made, precise, decidable verification proposition. Nobody has to write the proposition; a human only has to translate the test entry point into a verifiable goal. Three stages are therefore chained together:

existing test entry point (source of the assertion)
        ↓ automatic translation
formal proposition + precondition modeling
        ↓ automatic generation
proof script / lemma sequence
        ↓ machine checking (cheap, fast, decidable)
proof accepted / counterexample (feeds straight back as a regression test case)

Assembly-level verification adds further value. A proof at the source level does not mean the shipped binary is correct: instruction selection, alias analysis, the actual consequences of undefined behavior, inline assembly, and width or sign-extension handling can all introduce deviations invisible at the source level. Verifying at the machine-code level brings the “compiler-to-hardware” segment into the model — which is exactly the layer where many genuinely exploitable vulnerabilities live.

There is also a deeper, easily overlooked reason why “AI generation” matters at this moment:

The asymmetry of verification. Checking whether a proof is correct is mechanical, cheap, and takes milliseconds to minutes. Constructing a proof is expensive and requires insight. Once the generation side can iterate at scale, the expensive half gets amortized.

This does not mean generated output can be trusted as-is. The opposite: precisely because generation is cheap, a mandatory machine-checking gate must be in place. That is the engineering precondition for the whole approach.

5. Four Layers of Impact on Software Security

Layer 1: Defect discovery moves from “statistically confident” to “logically free of this defect.” For code whose input comes from an untrusted network — parsers, codecs, protocol stacks — an exhaustive proof of memory safety puts the risk in a different class than a passing test suite. Hundreds of newly found defects, some latent for years and surviving trillions of random inputs, directly confirm that the blind spots of sampling are real and substantial.

Layer 2: Cost tiering makes selective high-assurance achievable for critical code. Verification is no longer all-or-nothing. A sensible strategy ranks modules by exposure surface and consequence of failure and fully verifies only a few high-risk ones. This shifts security investment from “broad audit of the whole repository” to “deep proofs on critical paths,” substantially improving risk reduction per unit of cost.

Layer 3: Verifiable artifacts become a new deliverable. Traditional supply chains deliver code, dependency manifests, and build outputs. Adding machine-checkable proofs extends the deliverable to “certain security properties are proven for a specific code version.” This creates a new evidence class for audits, third-party assessments, and regulatory compliance — independently re-checkable logical assertions rather than sampled test reports.

Layer 4: Organizational structure and talent profiles change. Formal verification experts were a scarce resource, and their working mode was “complete the whole proof by hand.” Under the new paradigm the expert role shifts toward defining security properties, judging whether propositions are meaningful, reviewing whether model assumptions hold, and handling the hard cases where automated tools stall. Ordinary engineers are now expected to understand which properties were proven, and under what premises.

6. Adoption Path: Wiring Proofs into the Development Pipeline

If proofs are treated as one-off research, their value decays quickly. Sustained returns require treating them as engineering.

Tier the choice of verification targets. A reasonable ordering criterion: does input come from an untrusted source → does failure affect security or data integrity → is the code’s change frequency low (low proof maintenance cost) → does a test entry point already exist.

Tier	Target code characteristics	Recommended approach	Acceptance criteria
L1	General business logic	Fuzzing + static analysis + unit tests	Coverage and defect trends
L2	Untrusted input parsing, protocol handling	Bounded model checking + property-based tests	No counterexample on key properties
L3	Cryptographic primitives, memory management, permission checks	Exhaustive deductive verification + machine checking	Proof checking passes and proposition review passes

Connecting verification tasks to regular CI. Proof generation takes an unpredictable amount of time; checking is fast and deterministic. The two must be split:

stages:
  - name: build-machine-code      # retain verifiable target artifacts and debug info
  - name: generate-proof          # long-running; async / nightly / elastic compute
    artifacts: [ proof-bundle ]   # proofs, models, assumption list, version fingerprint
  - name: check-proof             # hard gate: a failed check blocks the merge
  - name: counterexample-regression  # counterexamples auto-converted into regression cases

Generated artifacts from the proof stage can be archived in object storage, and the verification tasks themselves suit containerized batch execution on elastic compute, with status and failure reasons consolidated through logging and monitoring/alerting. These are all standard cloud platform capability categories; no specialized infrastructure is required.

Versioning proofs and regression. Every proof must be bound into a fingerprint together with three things: the code version, the build configuration, and the model assumptions. After a code change, the pipeline re-verifies only the affected portion and reports an incremental conclusion on whether each proof still holds. Treating proofs as first-class deliverables under version control is the decisive factor in whether this system can be sustained.

Metrics. Recommended tracking: proven properties / target properties, proof invalidation rate (re-verification failures caused by code changes), machine-check pass rate, average generation time and compute cost, and the change in historical defect density per proven property. Without these metrics, verification work easily degrades into “it ran, so it passed.”

7. Six Boundaries and Risks That Must Be Confronted

1. The specification itself may be wrong. A proof only guarantees “the code conforms to the proposition.” If the proposition is written incorrectly, you get a rigorously proven wrong conclusion. Property review must remain a human responsibility and must not be delegated to the generation side.
2. Model gaps. Hardware faults, concurrency scheduling assumptions, external dependency behavior, allocator returns, system call semantics, timing and temporal properties, and side channels are typically outside the model. “Proven secure” is not the same as “secure once deployed.”
3. Trusted computing base (TCB) issues. If the checker, the solver, the formal semantics definitions, or the preprocessing and translation toolchain contain defects, the strength of the proof is weakened. These components require independent auditing, not assumed trustworthiness.
4. Vacuous proofs. Preconditions that are too strong (for example, assuming inputs are always well-formed), assertions that are too weak, or unproven intermediate steps all produce “passed, but proved nothing.” A passing check does not mean the proposition is meaningful.
5. Maintenance cost migrates into CI. Proofs are sensitive to code changes, and modules with high change frequency may never keep a proof valid for long. The tiering strategy must state early in a project “which code commits to remaining verifiable,” treating it as an architectural constraint rather than a later patch.
6. Unreliability of the generation side. Automatic generation may produce syntactically valid but semantically invalid proof paths, or depend on unproven environmental assumptions. All generated results must pass machine checking, and a minimal evidence chain that a human can review must be retained.

8. The Takeaway

The real significance here is not that “a model wrote a lot of code.” It is that the marginal cost of formal verification has been pushed down to a level where it can enter day-to-day development. Sampling tests answer “probably fine in probabilistic terms”; exhaustive proofs answer “logically impossible under this set of assumptions.” Neither can replace the other, but they can divide labor clearly: testing keeps carrying broad coverage and regression protection, while proofs concentrate on shoring up a small number of critical properties.

The practical advice for engineering teams is plain: start with modules that satisfy three conditions at once — an existing test entry point, untrusted input parsing, and memory safety — then bring proof artifacts under version control and CI gates, while establishing human checkpoints for property review and model assumption review. Prove a small number of genuinely important things first, and only then consider widening the scope. That is far more pragmatic than pursuing whole-repository verification in one shot.