Formally Verified AI-Generated Code: What Engineering Leaders Need to Know Before Trusting Agents in Production

Engineering leaders evaluating AI coding tools are mostly asking the wrong question. Speed of generation and benchmark scores are measurable and easy to compare, but they tell you nothing about whether the code will behave correctly under conditions the test suite did not anticipate. The more consequential question is what guarantees, if any, accompany the output. Formal verification offers a technically rigorous answer to that question, and new research makes clear that current agents are nowhere near ready to provide it at the scale that production systems require.

Companion piece to our broader work on AI coding agent reliability at scale. See Repository Context: The AI Coding Stack Bottleneck for why multi-module context failures are the structural constraint most teams underestimate.

What Formal Verification Actually Guarantees

Formal verification is not a more thorough form of testing. A test suite checks that a function produces the expected output for a finite set of inputs. A formal proof checks that the implementation satisfies its specification for every possible input, exhaustively, using machine-checked logic.

The distinction matters practically. A unit test on a cryptographic function might cover hundreds of edge cases and still miss a timing side-channel or an integer overflow that only surfaces under specific hardware conditions. A proof that the function satisfies a formally stated correctness property rules out entire classes of failure, not just the ones the test author thought to include.

The practical implication is that verification and testing are complementary, not substitutes. Verification eliminates logical incorrectness relative to a specification. Testing remains necessary to validate that the specification itself captures the intended behaviour, and that the runtime environment matches the model the proof assumes.

The Benchmark Gap Current Agents Cannot Close

Most existing AI coding benchmarks measure whether an agent can generate code that passes unit tests or produce a proof for a pre-written implementation. Neither of these captures what production software actually requires, which is coherent implementation and proof choices made jointly across a multi-module codebase.

The Vero benchmark, introduced to address this gap, evaluates exactly that. It contains 43 multi-module instances drawn from real repositories spanning cryptographic protocols, distributed systems, and other high-assurance domains, with each instance requiring an agent to produce both working code and a machine-checked proof in Lean 4 (Lou et al., arXiv 2026). The results from evaluating frontier coding agents are instructive: the strongest configuration fully solved only 27 of the 43 instances, and produced no closed specifications on the hardest repositories.

That 63% solve rate sounds plausible until you consider what the unsolved instances represent. The failures are not on trivial problems. They are concentrated on the repository-level instances where cross-module reasoning is required, which is precisely the structure of the software that most needs correctness guarantees.

The Function-Level to Repository-Level Gap

There is a structural reason why agents perform adequately on isolated function proofs but struggle at the repository level. A single function proof requires the agent to reason about one specification, one implementation, and one local context. A multi-module repository requires consistent choices about data representations, interface contracts, and invariants that must hold across module boundaries.

When an agent makes an implementation choice in module A that is locally valid but incompatible with the specification of module B, the proof for the system as a whole fails. The agent must then backtrack, revise, and maintain coherence across a context that may span thousands of lines. Current agents handle this poorly because their context management and planning capabilities were not designed around the constraint that every local decision has global proof consequences.

This is not a problem that will be solved by larger context windows alone. Repository-level verification requires a form of structured, hierarchical reasoning about dependencies that is architecturally distinct from next-token prediction over a long prompt. The gap is real and should be treated as a design constraint, not a temporary limitation.

What This Means for Your Deployment Decisions

The practical implication for engineering leaders is that the appropriate trust model for AI-generated code varies significantly by use case, and formal verification status is the most reliable discriminator.

For regulated industries, the calculus is straightforward. Medical device software, financial infrastructure, and safety-critical control systems operate under regulatory frameworks that require demonstrable correctness guarantees. AI-generated code that has not been formally verified, or that was verified only at the function level, does not satisfy those requirements. Treating benchmark performance as a proxy for regulatory compliance is a category error.

For high-assurance environments outside formal regulation, such as cryptographic libraries, authentication systems, or distributed consensus protocols, the Vero results suggest that current agents should be treated as accelerators for human engineers, not autonomous producers. An agent that solves 63% of repository-level verification problems is genuinely useful for generating candidate implementations and partial proofs. It is not ready to operate without expert oversight on the 37% it cannot close.

For general enterprise software where the failure mode is a degraded user experience rather than a safety event, the risk calculus is different, and supervised deployment of AI-generated code is already reasonable. The key discipline is being explicit about which category each system falls into, rather than applying a uniform policy across the codebase.

How to Factor Correctness Into Tool Selection

When evaluating AI coding tools for production use, the first question to ask vendors is what verification artefacts, if any, accompany the generated code. A tool that produces only code and unit tests provides a different assurance level than one that produces code, tests, and a formal proof. Most current tools provide the former.

The second question is at what granularity verification is performed. Function-level proof generation, which several tools now support, is meaningful but insufficient for systems where correctness depends on inter-module contracts. Ask vendors specifically whether their tooling has been evaluated on multi-module verification tasks, and what the solve rates look like on benchmarks like Vero rather than on isolated function problems.

The third question is about the specification authorship process. A proof is only as strong as the specification it verifies against. Specifications written by the same agent that generates the implementation create a circularity risk: the agent may produce a proof that a correct implementation satisfies an incomplete specification. Robust verification workflows require human-authored or human-reviewed specifications, particularly for the interface contracts between modules.