The Case for Formal Verification in the Agentic Development Era

Who am I?

My name is Alex and I’m a software engineering intern at Nuvo. I’m a third-year at Carnegie Mellon University studying Math and Computer Science. I’m mainly interested in applying the highly abstract fields of analysis and logic to important practical settings. At Nuvo, I’ve been enjoying working on improving the identity verification model and expanding customization for the application’s core dashboard interface.

Introduction

It's no debate that the capabilities of AI agents have exploded over the last few years and will continue to explode over the coming years. What's still relatively unknown is what role these agents will play in the economy and how they will be utilized by businesses.

Here is what we do know: software complexity is growing faster than engineers can handle. As that complexity grows, humans tackle more meta, abstract problems surrounding the product and delegate the rest to agents. It’s become increasingly apparent that most software components at the industry level can be made by AI agents at a fraction of the cost. I imagine most engineers have contemplated and reconciled with a future where engineers hand off their lower-level work to AI agents. In this article, I argue that formal verification is the missing piece for AI-assisted development, and walk through what that looks like in practice.

Current Limitations

The primary issue businesses face with these agents is that there's no way to verify their output’s correctness without reading it yourself. In a few prompts Claude can define a database schema, wire up endpoints, and build an interactive UI, but the output is never quite right and the code is hard to read. Engineers still have to verify every line before it ships. The work has shifted from writing code to reading it.

The gap between what we want the model to produce and what it actually outputs is largely a failure of specification. Research from Stoica et al. argues that the lack of precise specifications is the fundamental bottleneck preventing LLM systems from being engineered with the same rigor as traditional software, and Hu et al. have shown that a large class of LLM failures trace directly back to identifiable prompt defects, missing context, ambiguous instructions, and under-constrained formatting.

The development of skills, reusable instruction files that give agents project-specific context, is a practical attempt at standardizing this. Skills have already dramatically accelerated development, but they have a fundamental limitation: they get out of sync with the project almost immediately. As the codebase evolves, the assumptions baked into a skill silently become stale, and there is currently no mechanism to track or detect that drift. Further, even if every skill were perfectly maintained, model performance dramatically drops off in multi-file systems and we still haven’t solved the interoperability problem, so we have to keep the skills relatively self-contained and read model output.

The question is not how to make agents smarter. We've all seen what they can do on their best runs. The question is how to eliminate their ability to produce incorrect output. We’ve already abstracted away the bytecode that is actually run post compilation, so who is to say we can’t abstract away more about the software we write?

A Model for Agent-Operated Software

Every software system, regardless of complexity, can be decomposed into three concerns: what external dependencies it relies on (the dependency layer), what the system actually does (the implementation layer), and what rules the system must follow (the specification layer). Today, humans own all three. As formalization matures, agents move from implementing code that humans verify by reading it, to implementing human- defined specification in the implementation layer, to automatically identifying dependency layer issues and resolving them, to eventually owning entire applications. This is the trajectory we are on.

In practice, there is a natural ceiling to how far this goes for human-facing software. As long as a human is responsible for what the software does, they will likely want other humans monitoring nondeterminism, side channels, and other external dependencies at the dependency layer. Hardware behaves in ways formal proofs cannot fully capture, third-party providers change their behavior without notice, and network conditions are inherently unpredictable (although this is changing). These are problems that require human judgment to manage. Further, if software is being used by humans, there is a cultural expectation that other humans understand how the system works and make decisions about how it interacts with people. Interface design, accessibility, regulatory compliance, and product direction are not things most organizations will hand to agents regardless of how capable they become. For human-facing software, humans likely never fully leave dependency and specification. While there are ideas of agents operating all layers, they are too hypothetical for this discussion. The practical question is what it takes to eliminate incorrect output so that agents can move from reading-and-checking to autonomously owning the implementation layer.

Formalization

Formalization is not binary. It is a spectrum from verifying function input types all the way to a full mathematical proof of correctness in a language like Lean. Most software today already sits somewhere on this spectrum: type systems, schema validation, and contract checks are all lightweight forms of formal specification. As more of an application's behavior becomes automatically verifiable, we can delegate more of its implementation to an agent.

Kleppmann argues that these forces form a self-reinforcing cycle. AI-generated code can't be trusted without verification because LLMs are probabilistic, but formally verified code is correct by definition. The proof checker is a small piece of trusted code that rejects any invalid proof regardless of how it was generated, so it doesn't matter if the LLM hallucinates during proof generation. The verifier simply forces a retry. Crucially, LLMs are increasingly capable of writing these proofs themselves, which means AI both creates the demand for formal verification and supplies the labor to make it practical. Each improvement in model capability makes verification cheaper, and each advance in verification makes AI output more trustworthy.

The empirical evidence is already here. The vericoding benchmark (Bursuc, Tegmark et al., 2025) tested LLM generation of formally verified code across 12,504 tasks and found success rates of 82% in Dafny, 44% in Verus/Rust, and 27% in Lean using off-the-shelf models. Dafny verification improved from 68% to 96% over a single year. Notably, adding natural language descriptions to the formal specs did not significantly improve performance, supporting the thesis that the spec, not the prompt, is more important.

A lot of research groups are converging on this from different angles. Google DeepMind built AlphaProof, a reinforcement learning agent that generates formal Lean proofs and achieved silver medal performance at the 2024 IMO. DeepSeek released Prover-V2, an open-source 671B parameter model for Lean 4 theorem proving that hits 88.9% on the MiniF2F benchmark. Harmonic and ByteDance both fielded strong results at the 2025 IMO. Microsoft Research maintains both Lean (the language itself) and F*, and used F* to ship a verified TLS stack in production browsers. On the startup side, Axiom Math raised $200M to build a Lean-based verification engine.

Once the spec is satisfied, agents can continuously optimize the implementation in the background, minimizing for program length, modularity, cost, latency, or other properties. This idea was first developed by my friend at CMU and has since been picked up by Meta researchers. There is also a rich area of research using Lean for compiler optimization.

Limitations of this Framework

Not all software is equally amenable to this model. Software that is fully formalizable (protocol compliance, algorithmic correctness, cryptographic properties) works today. Software that is parametrically formalizable (correct structure but human-tuned values like timeouts, retry policies and UI design) is possible but requires more work.

Even where formalization applies, as Chlipala outlines, proofs may rely on assumptions that are not true due to side channels and nondeterminism, and this compounds with each new block of agent-written code. The framework also assumes formal spec libraries will exist, but their maturation is a community coordination problem gated by different dynamics than AI capability growth. Writing specs is harder than writing implementations. If the spec of a core axiom of a product changes, the trickle down effects can become arbitrarily large. Formal dependency tracking and agent rebuilds help, but foundational changes like Spectre-class discoveries trigger massive re-verification whose speed is an open question.

Example

As a part of Nuvo’s trade network, users interact with a multi-step, extensible application system. In a customer application, a supplier configures which steps are required, and the application moves through a series of statuses as the buyer populates it with more information. The following is a hypothetical formalization in Lean 4, not production code, but an illustration of how a step and submissions properties like this could be expressed and machine-checked.

The data model mirrors what you would see in a typical Python definition but uses Lean's syntax:

structure Company where
id : PrimaryKey
legalName : Option String
claimed : Bool

inductive Step where
| companyDetails
| shippingLocations
| taxExemptions
| tradeReferences
| bankReferences
| personalGuaranty
| additionalResponses
| confirmation
| verification

opaque StepData : Step → Type

inductive ReviewStatus where
| incomplete
| application

structure CustomerApplication where
id : PrimaryKey
buyerId : ForeignKey Company
supplierId : ForeignKey Company
reviewStatus : ReviewStatus
requiredSteps : Set Step
completedSteps : Set Step
stepData : (step : Step) → Option (StepData step)

structure AppState where
apps : Set CustomerApplication

The data model mirrors what you would see in a typical Python definition but uses Lean's syntax. A CustomerApplication belongs to a buyer and supplier through foreign keys, tracks which steps are required and which are completed, and stores typed data for each step. StepData is opaque and parameterized by Step, so the type system enforces that each step can only hold the correct kind of data. With the data model defined, we can write functions whose return types guarantee properties about the resulting state:

def app (s : AppState) (appId : Nat) : CustomerApplication :=
s.apps.find appId

def submitStep (s : AppState) (appId : Nat) (step : Step) (data : StepData step)
: { s' : AppState //
(app s' appId).stepData step = some data ∧
step ∈ (app s' appId).completedSteps }

def submit (s : AppState) (appId : Nat)
(h : (app s appId).requiredSteps ⊆ (app s appId).completedSteps)
: { s' : AppState //
(app s' appId).reviewStatus = .application }

With the data model defined, we can write functions over AppState whose return types guarantee properties about the resulting state. submitStep takes an application, a step, and the correctly typed data for that step, and returns a new state where the data is persisted and the step is marked complete. submit takes an application where every required step has been completed and returns a new state where the ReviewStatus is application. In plain English, any code path that calls submit must first prove that all required steps are done, and any code path that marks a step as done must first provide the actual data for it. The chain of proofs flows from the database layer up through the business logic, so if either function is called incorrectly the code will not compile.

Because bugs like missing step data or premature submissions appear all the time, keeping these constraints as CI checks can rapidly improve the rate at which we can confidently push changes. And because the spec lives in the type signatures rather than in runtime assertions, an agent can freely swap out the implementation underneath without touching the guarantees. This kind of specification requires dependent types because the return type of submitStep references the specific state being returned, something languages like Python, Rust, or Haskell cannot express in their type systems.

Integration into Business Applications

Despite the capabilities mentioned, anyone trying to integrate formal software into their core product is running into a big issue: under-developed tooling for Lean and other formalized software languages. These languages were primarily made for mathematicians and compiler engineers and don’t have mature libraries for practical software engineering. I’ve started a project called SWELib which aims to build useful, open source Lean tools for developers aiming to try to adopt this model of software engineering, but the project is still in its infancy.

Conclusion

AI agents are perfectly capable of accelerating application development far beyond where it is today, but there is a fundamental bottleneck in the process as long as we can't trust the code that's written. At Nuvo, we're constantly experimenting with new automation techniques through both application structure and agent workflows, and the two reinforce each other naturally. The more precisely we define what our software should do, the more confidently we can delegate how it gets done. The sooner the broader engineering community invests in that foundation, the sooner we stop babysitting our agents and start collaborating with them.

I've loved getting to work on these problems firsthand at Nuvo, from identity verification to thinking about what it'll actually take to trust agent output at scale. If these kinds of problems excite you, come join us.