When one AI writes the specification, the code and the proof, a single mistake can run through all three and still be verified.
The AI pipeline for formally verifying software is seductive. A developer describes what they want in plain language. A model writes a formal specification. The same model writes an implementation. The same model writes a proof that the implementation satisfies the specification. A proof checker confirms it. Out comes software carrying a machine-checked guarantee, produced in minutes rather than the expert-years that formal verification used to demand.
But that guarantee is narrower than it sounds. A proof establishes that the code satisfies the formal specification, under the assumptions encoded in the verification model. It says nothing about whether the specification captures what the developer actually intended. And when one model writes the specification, the code, and the proof, a single misunderstanding can propagate from the specification into the implementation, while a perfectly valid proof certifies that the two agree. The question the whole pipeline skips is the one that matters most: who checks the specification? Lean’s creator, Leonardo de Moura, says that as AI takes over implementation, “specification becomes the core engineering discipline.”
Verified Against the Wrong Thing
A proof establishes that an implementation satisfies a formal specification, under the assumptions built into the verification model. What it does not establish, by itself, is that the specification captures the behavior anyone actually intended. The most extreme form of this failure has a name in the verification literature: vacuity, a term introduced in hardware model checking in the late 1990s and since carried over to software verification. A specification is vacuous when it holds for a trivial reason, for instance because the condition that would trigger it never occurs, rather than because the system behaves as intended. A postcondition can be trivially true, asserting nothing a program could fail to satisfy. A precondition can be quietly self-contradictory, so that no input ever meets it and any claim conditioned on it can be proved. A function marked “requires false” will verify against any postcondition at all, because no input is ever allowed to reach it.
This is not a theoretical worry. KaPilot, a July 2026 system that uses LLM agents to write specifications for Amazon’s Kani verifier for unsafe Rust, treats it as a first-order problem. A generated specification can satisfy the verifier while holding only for trivial reasons, so KaPilot builds in a dedicated check: it adds a deliberately impossible guarantee, and if the verifier still passes, the specification was asserting nothing. Its authors note that evaluating specification quality “is hard to automate systematically”; the check exists for exactly that reason. A 2026 study of LLM-generated code verified in the Dafny language describes the same failure as vacuous verification, where a model satisfies the verifier with weak or trivial specifications that do not solve the intended problem. And a third group, SpecSyn, observes that existing LLM-based tools “are typically equipped with no mechanisms to evaluate and guarantee the strength of the generated specifications,” meaning how precisely they pin down real program behavior.
Models also have an incentive to find such shortcuts. METR has documented OpenAI’s o3 exploiting flaws in scoring code in roughly 30% of runs on one suite of AI research tasks, and the ImpossibleBench study found GPT-5 exploiting test cases in 76% of coding tasks deliberately constructed so they could not be solved honestly.
The Specification Gap
In VeriContest, a May 2026 benchmark built on Verus, a verification tool for Rust, the verification pipeline is broken into stages and each stage is scored independently. The pattern is consistent across models: they write code far better than they write specifications. OpenAI’s GPT-5.5 reached roughly 92% on turning natural language into code, about 48% on turning the same natural language into a specification, and around 5% end-to-end. Anthropic’s Claude Opus 4.7 cleared 90% on code, about 21% on specification, and just over 2% end-to-end. The proof stage was hard for both, at roughly 14% and 13%. CLEVER, a hand-curated Lean benchmark of 161 problems designed to exclude vacuous solutions and specifications that leak implementation logic, likewise illustrates the difficulty. The original 2025 evaluation found that no method tested solved more than one problem end-to-end, although newer agentic approaches have since improved substantially.
These results locate the difficulty. Models are far better at writing code than at writing specifications or proofs. But specifications and proofs fail differently: an invalid proof is rejected by the proof checker, while a valid proof can still certify the wrong property if the specification fails to capture the intended behavior. This is the gap Chris Hsu has pointed to. Hsu, the founder of Kilometre Capital and the family office Rocketeer Management, supports formal verification research through his Infinitude Foundation.
Hsu has argued that more attention and investment should move toward the specification layer. A proof checker can mechanically reject an invalid proof, but even a valid proof cannot establish that the specification captures what was actually intended. An important part of that challenge is the underlying formal vocabulary. AI’s advances in formal mathematics have benefited from Mathlib, a vast, community-developed library of formal definitions and theorems that provides a shared foundation for mathematical reasoning in Lean. Software verification does not yet have an equivalent knowledge base at comparable scale, making it harder for AI to express intended software behavior using shared, reusable and well-vetted formal definitions. Open-source efforts such as CSLib, which explicitly aims to be for computer science what Mathlib is for mathematics, are beginning to build that missing infrastructure.
The Independence Problem
Redundancy protects against error most effectively when the redundant components fail independently. That is why safety-critical engineering uses dissimilar redundant systems and why a paper is sent for review to referees who did not write it. A specification and an implementation produced by a single model share training data, inductive biases and, most importantly, a single reading of the prompt. A machine-checked proof is different: an independent proof checker can establish that the implementation satisfies the formal specification, but it cannot establish that the specification captured the intended behavior. In a classic 1986 experiment, John Knight and Nancy Leveson found that 27 independently written versions of one program failed together far more often than independence predicts. A June 2026 replication with AI coding agents found the same pattern, though majority voting across versions still cut failures substantially, and across more than 350 language models, two models that both err on standard multiple-choice benchmarks pick the same wrong answer about 60% of the time.
Consider a system meant to restrict access to authorized users. If the model misconstrues what the requester meant by authorized, it will encode that misconstruction in the specification, honor it faithfully in the code, and prove the two consistent. In that case, every formal stage can pass. The proof checker certifies precisely what it was asked to certify, which is the problem. The error stays invisible at every point where a check occurs, because it lives upstream of all of them.
The result is worse than an unverified program in one specific respect. It carries a stamp of approval. As the ratio of certified claims to adjudicated claims widens, certification stops carrying information about whether anyone has judged that a claim means what it says, while remaining a perfectly reliable signal about derivation. Maher Kallel and Mohamed El Louadi, analyzing the same decoupling in machine-checked mathematics, argue that “nothing in the argument is specific to mathematics”: in software and cryptography, “the correspondence is the specification, and the transfer is exact.”
What the Fixes Can and Cannot Do
Several fixes have been proposed. Vacuity checking can be enforced as a gate, so that a specification passing the verifier must also be shown non-trivial, which is KaPilot’s approach. Specification strength can be measured by mutation: generate program variants, then test whether the specification can tell them apart, as SpecSyn does. Drift between what was asked and what was formalized is caught by held-out human ground-truth specifications with equivalence proofs, the CLEVER design, though that reintroduces dependence on human-written references that are expensive to produce and can carry bias of their own; a 2026 study adds that such equivalence proofs are hard enough to “conflate proof difficulty with specification quality.” Assigning different models to different stages breaks some of the correlation, though less than vendor diversity suggests, and at the cost of the coherence that made the single-model pipeline attractive.
These approaches help, but they do not eliminate the specification problem. They move the hardest question upstream: whether the formal properties being proved actually capture the behavior the system is intended to have. AI may increasingly generate the specification, the code and the proof, but its work should never be accepted on its own word.
From Intent to Proof
Hsu has framed the broader constraint on agentic systems as a distinction between probabilistic confidence and mathematical proof: 99% confidence is fundamentally different from an independently checkable proof, particularly when AI systems are given authority over consequential software and infrastructure. On verification, his position starts one step earlier. The critical question is whether the formal specification faithfully captures the intended behavior. AI may increasingly automate the translation from intent into specifications, but a proof alone cannot establish that the specification expresses the right requirements.
From there, the trust chain must remain independently checkable. The system generating code or proofs need not itself be trusted if the resulting proof can be checked independently against the specification by a small, trusted proof checker. Hsu’s Infinitude Foundation funds the field directly, with verification grantees including the Stanford Center for AI Safety and the Lean FRO, which develops Lean under Convergent Research. Lean’s creator Leonardo de Moura makes the same argument: “Independent verification is not a philosophical preference. It is a security architecture requirement.”
The optimistic case is worth taking seriously. Specification generation is improving rapidly, and the relevant comparison is not only with carefully human-specified software, but with the growing volume of AI-generated code that ships without formal verification at all. Vacuity is also a precisely defined defect, and it can often be detected automatically. But existing techniques still cannot, by themselves, establish that a formal specification faithfully captures the intended behavior. AI may increasingly automate specification generation and evaluation, but the specification-intent gap remains.
Hsu’s answer is to make the entire chain more trustworthy: specifications grounded in open, community-vetted formal definitions; proofs that can be independently checked rather than taken on trust; and a verification architecture that does not require trusting the system or company that generated the code. AI may increasingly generate the specification, the code and the proof. The critical distinction is that it should never simply be asked to trust its own work. Verified by whom? The proof can be checked by anyone. The harder question is whether what was proved is what we intended in the first place.
