The Proof Got Cheap. The Specification Didn't: What AI-Driven Formal Verification Means for Your Engineering Team
Formal verification used to cost half a person-day of expert proof work per line of code. LLMs now write proofs that a machine checks, and a hallucinated proof simply fails. The catch is that proving code correct only helps if you specified the right thing, and that part is still on you.
Vibe Coding Has a Strict Sibling
For most of software history, formal verification has been something engineers respect and almost nobody does. You write a precise mathematical specification of what a program should do, then produce a proof, checked by a machine, that the implementation meets it. The result is a much stronger guarantee than any test suite can give. The cost has been so high that it was reserved for microkernels, cryptographic libraries, aircraft software and a handful of cloud infrastructure teams.
In December 2025, Martin Kleppmann, author of Designing Data-Intensive Applications, published a short post titled Prediction: AI will make formal verification go mainstream. His argument has three parts: AI is about to make proofs much cheaper to write, AI-generated code needs a way to be trusted without a human reading every line, and the precision of formal methods balances the probabilistic nature of language models. The post spread widely through engineering circles, and over the following ten months the idea moved from prediction to active product and research work.
The research community has even coined a name for it. A September 2025 paper introduced vericoding, LLM generation of formally verified code from formal specifications, and explicitly contrasted it with vibe coding, which produces potentially buggy code from a natural-language description. That contrast captures the current mood well. Developer forums are full of frustration with agent-written code that looks right and isn't. Vericoding offers a different deal: let the model write the code and the proof, and let a small, trusted checker decide whether either is acceptable.
This article is about what that shift means for ordinary engineering teams, not research labs. The short version is that the cost of proving has fallen sharply, the cost of specifying has not, and the teams that understand the difference will get the benefit while the others buy tools they cannot use.
Why the Economics of Proof Just Changed
The reason formal verification stayed niche is simple arithmetic. Kleppmann's post uses the classic example: the seL4 microkernel was about 8,700 lines of C, and proving it correct took roughly 20 person-years and about 200,000 lines of Isabelle proof. That works out to around 23 lines of proof and half a person-day of expert effort for every line of implementation. He also estimates that only a few hundred people in the world can write proofs of that kind. For almost every commercial system, the expected cost of bugs was lower than the cost of preventing them this way.
Language models change the cost side of that equation, and they do it in an unusually safe way. When an LLM writes application code, a hallucination can ship to production unless a human or a test catches it. When an LLM writes a proof, the proof checker either accepts it or rejects it. As Kleppmann puts it, it does not matter much if the model produces nonsense, because the checker refuses invalid proofs and the model has to try again. The checker is a small, well-understood program, so trusting it is very different from trusting the model.
That property is exactly what makes formal methods attractive in the age of coding agents. The industry spent 2025 and 2026 learning that agents can produce code faster than humans can review it. Proof-checked code inverts the problem: the agent can be as unreliable as it likes during the search, as long as the final artefact passes a check that does not depend on the agent being honest or careful.
Money is following the idea. Harmonic, whose Aristotle system writes proofs in the Lean 4 proof assistant, raised a $120 million Series C at a $1.45 billion valuation, with Nvidia's NVentures among the investors. Most of that work is still aimed at mathematics rather than software, but the tooling, the training data and the proof engines carry over.
Key Takeaways
- Classic formal verification cost around half a person-day of expert proof work per line of code
- A proof checker rejects invalid proofs, so model hallucinations cost retries rather than bugs
- Machine-checked proofs let teams trust agent output without reading every line
- Investment in AI proof systems is rising, even though most of it currently targets mathematics
What the Benchmarks Actually Show
The headline numbers are good, but the spread between languages is the more useful signal. The vericoding benchmark, with 12,504 specifications across Dafny, Verus/Rust and Lean, found off-the-shelf models succeeded on about 82% of Dafny tasks, 44% of Verus tasks and 27% of Lean tasks. The same paper reports that model performance on pure Dafny verification rose from 68% to 96% in roughly a year. Dafny does a lot of the proof work automatically through its built-in solver, which makes it the friendliest target for models today.
Results on harder problems are lower. On the miniF2F-Dafny mathematical benchmark, the best model reached 62.7% cumulative pass@4, while Dafny's automation alone solved 39 to 44% of problems with an empty proof. That second number is a useful reminder: part of what looks like model capability is the underlying verifier doing its job, which is why choosing the right tool matters as much as choosing the right model.
Specification writing is the weak spot. A June 2026 study, Can LLMs Write Correct TLA+ Specifications?, tested 30 models on turning natural-language descriptions into TLA+, the specification language widely used for distributed systems design. Pooled across open-weight runs, the best prompting strategy produced specifications that parsed 26.6% of the time, and only 8.6% passed model checking. The authors concluded that current models do not generate reliable TLA+ specifications without expert oversight.
Put these results side by side and a clear pattern emerges. Models are getting good at proving that code meets a specification someone else wrote. They are still poor at writing the specification itself. That gap defines what teams should and should not delegate.
| Task | Benchmark | Reported result |
|---|---|---|
| Verified code generation in Dafny | Vericoding benchmark (2025) | About 82% success |
| Verified code generation in Rust with Verus | Vericoding benchmark (2025) | About 44% success |
| Verified code generation in Lean | Vericoding benchmark (2025) | About 27% success |
| Mathematical proofs in Dafny | miniF2F-Dafny | 62.7% cumulative pass@4 for the best model |
| Natural language to TLA+ specification | TLA+ generation study (2026) | 26.6% parse, 8.6% pass model checking (pooled open-weight runs) |
Where Formal Methods Are Already in Production
Formal methods are not new to the cloud. AWS engineers have used formal specification and model checking since 2011, as described in the 2015 paper How Amazon Web Services Uses Formal Methods. A 2025 follow-up by Marc Brooker and Ankush Desai, Systems Correctness Practices at Amazon Web Services, describes a portfolio that runs from TLA+ and the state-machine-based P language through deductive verification to property-based testing, fuzzing and runtime monitoring. One detail stands out for anyone planning adoption: AWS created P partly because many engineers found TLA+ hard to learn once formal methods spread beyond the original teams.
Authorization is the area where verified code is furthest along. Cedar, the policy language behind Amazon Verified Permissions, was designed so that policies could be analysed by reduction to SMT, a type of automated logic solver. A 2026 Amazon Science paper on SymCert describes a framework written in Lean that verifies the analyses themselves, and reports verifying five analyses used in an AWS Cedar analysis service. In other words, the tool that tells you what a policy permits has its own correctness proof.
The same reasoning engines are now moving into AI products. Amazon Bedrock's Automated Reasoning checks became generally available in August 2025, with AWS claiming up to 99% verification accuracy for checking model answers against formalised policies. That is a vendor figure and it applies to content the policy actually covers, but the design choice is telling: the check is done by logic, not by another model.
The most relevant development for software teams arrived in May 2026, when The New Stack reported on Requirements Analysis in AWS's Kiro. An LLM rewrites loose requirements into precise criteria, translates them into formal logic, and an SMT solver checks them for contradictions, ambiguities and gaps before any code is written. AWS found problems in roughly 60% of first-draft requirements in its own testing. That is an internal number, but anyone who has worked on a large project will find it believable.
Key Takeaways
- AWS has used formal specification and model checking since 2011 and now runs a broad portfolio of formal and semi-formal methods
- Authorization policy analysis is the most mature area, with Lean-verified analyses in production
- Automated reasoning is moving into AI products and coding tools, checking requirements before code exists
- Vendor accuracy figures apply to well-formalised cases and should be read that way
The New Bottleneck Is the Specification
Kleppmann identifies the problem that will define this field for ordinary teams: once proofs are cheap, the hard question becomes how you know the properties that were proved are the properties you actually cared about. A proof that a function sorts a list says nothing useful if the specification forgot to require that the output contains the same elements as the input. A verified system that meets the wrong specification is wrong with a certificate.
This is not a theoretical concern. The TLA+ study above shows models producing specifications that look valid and fail on meaning. The Kiro results show the same thing at the requirements level: most first drafts contain contradictions or gaps that nobody noticed. The gap between what stakeholders mean and what is written down was always the main source of serious software failures. Cheap proofs do not close that gap. They make it the only gap left.
Datadog's engineering team put a number on the effort. In a March 2026 post on building systems with agents behind a verification harness, it reported that writing the invariants and specifications took roughly two to three times the effort of writing the code itself. The post's summary of the situation is blunt: the bottleneck has moved from writing code to trusting what was written. Datadog's answer was to put human effort into defining the system and its invariants, then let automated checks replace line-by-line review.
For engineering leaders, this changes what a strong engineer looks like. The valuable skill is no longer typing an implementation quickly. It is stating precisely what a component must and must not do, including the edge cases a product owner never mentioned. That skill has always separated senior engineers from the rest, and it is the part of the job AI is least able to take over.
A Verification Ladder for Teams That Are Not AWS
Most teams should not start by writing Lean proofs. Formal verification is the top rung of a ladder, and each rung below it gives a useful share of the benefit at a fraction of the cost. Datadog's Helix project, a Kafka-compatible streaming engine built largely by coding agents, is a practical example. Its verification pyramid combined TLA+ specifications for understanding, deterministic simulation testing as the main check, exhaustive model checking, bounded proofs with the Kani Rust verifier, and production telemetry as the final source of truth.
The deterministic simulation layer found the kind of bug that justifies the whole approach. According to the same Datadog post, a write-ahead log truncated its in-memory state before the on-disk sync completed, so an injected disk fault meant the segment was never retried and data was lost. That is a classic distributed systems failure: rare, silent and almost impossible to catch in code review. A simulation harness running seeds automatically found it, and an agent could then fix it against a check that would tell it whether the fix worked.
For a typical product team, the practical ladder looks like this. Start with property-based tests that state invariants instead of examples. Add deterministic simulation and fault injection for anything with concurrency, retries or distributed state. Use a model checker such as TLA+ or P for protocols where interleavings matter. Reserve proof-based tools such as Dafny, Verus, Kani or Lean for small, high-value components where an error is very costly. AI now helps at every rung: agents write property tests, generate simulation harnesses and attempt proofs, while engineers own the invariants.
The common thread is that each rung turns a vague question, whether the code is right, into a mechanical check an agent can iterate against. That is the same property that made AI-driven migrations work, and it is why verification infrastructure is becoming a better investment than more code review hours.
| Rung | Example tools | Best suited to | Effort |
|---|---|---|---|
| Property-based testing | Hypothesis, fast-check, jqwik | Business rules, parsers, data transformations | Low |
| Deterministic simulation and fault injection | Custom simulators, Antithesis | Retries, queues, storage, distributed state | Medium |
| Model checking | TLA+, P, Stateright | Protocols, consensus, workflow state machines | Medium to high |
| Bounded verification | Kani, CBMC | Unsafe code, memory handling, numeric edge cases | Medium |
| Full proof | Dafny, Verus, Lean | Authorization, cryptography, financial calculation cores | High, falling quickly |
Key Takeaways
- Formal proof is the top rung, and most teams get most of the value from the rungs below it
- Deterministic simulation catches rare, silent failures that code review misses
- Each rung converts the question of whether code is correct into a check an agent can iterate against
- AI writes the tests, harnesses and proofs, while engineers own the invariants
What to Verify First, and What to Leave Alone
Formal methods pay off where three conditions hold: the logic is compact, the rules can be stated precisely, and a mistake is expensive or hard to detect. Authorization is the classic example, which is why AWS invested so heavily in Cedar analysis. A single permissive rule can expose every customer's data, and the question of who can access what is precise enough to formalise. Pricing and billing calculations, money movement, entitlement checks and data retention rules have the same shape.
The second strong candidate is concurrency and distributed coordination: job schedulers, idempotency and retry logic, leader election, synchronisation engines and anything that promises exactly-once behaviour. These are the components where agent-written code is most dangerous, because the bugs depend on timing and do not show up in ordinary tests. A model-checked specification of the protocol, plus simulation tests against the implementation, gives coverage that no amount of review can match.
The third candidate is requirements themselves. Even if you never prove a line of code, running critical requirements through a solver-backed check, as Kiro now does, catches contradictions while they are still cheap to fix. For regulated work, a precise specification also becomes useful evidence for auditors and customers who ask how you know a control works.
Equally important is what to leave alone. User interfaces, marketing pages, most CRUD screens and fast-changing product experiments rarely justify formal specification. Their requirements change too often and their failures are visible and cheap to fix. Spending specification effort there is how a promising practice gets a reputation as academic overhead.
Key Takeaways
- Verify compact, precisely specifiable logic where errors are costly: authorization, billing, entitlements, retention
- Model-check concurrency and distributed protocols, where agent bugs hide in timing
- Run solver-backed checks on critical requirements before any code exists
- Do not spend specification effort on UI, CRUD and fast-moving experiments
Where a Dedicated Team Fits
The constraint for most companies is not the tooling. Dafny, TLA+, P and property-based testing libraries are free, and AI assistance is already built into the tools teams use every day. The constraint is people who can write precise specifications, build simulation harnesses and judge whether a proof actually covers what the business needs. Those engineers are rare, and product teams rarely have the time to grow them while delivering a roadmap.
This is where a dedicated development team can help. At Stepto, we approach verification as part of delivery, not a separate research project. We start by identifying the small set of components where an error would be expensive, write explicit invariants with your domain experts, and then build the checks: property-based tests, deterministic simulation for distributed components, model-checked protocol specifications where the interleavings justify it, and proof-based verification for the narrow cores that need it. Agents then work against those checks, which lets you take on more AI-written code without adding the same amount of review time.
Serbian engineering has a strong tradition in mathematics and computer science, and our engineers work in time zones that overlap the full European working day and the US East Coast morning. That matters for specification work in particular, because the hardest part is the conversation with the people who know what the system must do. If you need one or two engineers to add verification to an existing team, staff augmentation is the lighter option. If you are building AI features that need the same discipline, our AI developers bring evaluation and verification practices to that work too.
The commercial case is straightforward. Every team using coding agents is already paying for verification, either through review hours, production incidents or both. Moving part of that spend into precise specifications and automated checks is how you keep the speed of agents without inheriting their error rate. If you want to scope where that would pay off in your system, talk to us.
Key Takeaways
- The scarce resource is people who can specify precisely and build verification harnesses, not tools
- Stepto builds invariants, simulation tests, model checks and targeted proofs as part of delivery
- Time zone overlap supports the specification conversations that matter most
- Moving review spend into automated checks keeps agent speed without agent error rates
Proofs Are Becoming a Commodity. Precise Intent Is Not.
AI is removing the main reason formal verification stayed niche. Models can now write proofs that a small, trusted checker accepts or rejects, which makes verified code one of the few ways to trust agent output without reading every line. The benchmarks show rapid progress on proving code against a given specification and weak results on writing the specification itself, and production experience at AWS and Datadog points the same way. The work that remains is deciding precisely what your system must do, for the few components where being wrong is expensive, and building the checks that hold agents to it. Teams that invest there will ship agent-written code with more confidence than teams that keep adding reviewers. If you want engineers who can write those specifications and build the verification harness around your most critical code, talk to Stepto about a dedicated team.
Building a team in Eastern Europe?
StepTo helps European and US companies build senior-led nearshore engineering teams in Serbia. Let's talk about what your next engagement could look like.
Start a conversationMore from StepTo on this topic
- The Specification Is the Source Code: Why Spec-Driven Development Is the Next Outsourcing Skill Gap
AI agents can build working software from a good spec. Writing specifications is now the critical skill, and most outsourcing vendors aren't ready.
- Half of Your S/4HANA Programme Is Ordinary Software Work. You Are Paying SAP Rates for All of It.
Only 39% of SAP's ECC customers had moved by the end of 2024. With mainstream support ending in 2027, the deadline is now a staffing problem, and a large part of the work does not need an SAP specialist.
- 84% of Developers Use AI. Only a Third Trust It. Here's What That Gap Is Costing Your Engineering Team
84% of developers use AI but only 32.7% trust it, and fewer than half always verify it before committing. Inside Stack Overflow's adoption-trust paradox.
Written by
Igor GazivodaFounder & CEO · StepTo
Igor has 15+ years in software engineering and business development. He specializes in scaling engineering teams, nearshore strategy, and AI-driven product development. He holds a Master's in Computer Science from the University of Belgrade.
LinkedIn →