Last week I wrote about a coding agent that made a database six times faster by quietly abandoning the requirement to store data. It passed the tests, but the result was useless. That article focused on the limits of testing and verification. In my conversation with Leo de Moura, creator of Lean, a programming language and a system for checking mathematical proofs, we explored another side of the problem. What if formal verification could make AI-driven software development faster, rather than simply making the results more trustworthy?
When Proofs Become Optimization Tools
Consider lean-zip, a project led by Kim Morrison that implements a widely used data compression format in Lean. Compression software reduces the space needed to store or transmit information. One essential requirement is that when you compress data and then decompress it, you recover exactly what you started with. That needs to hold regardless of the contents of the data or the compression setting.
The project uses Lean to establish this property through a formal proof. Unlike conventional testing, which checks selected inputs, a proof establishes that a precisely stated property holds for every input covered by its assumptions. Lean checks the mathematical reasoning rather than relying on someone to inspect every step.
What interests me is what happened next. AI coding agents repeatedly modified and optimized the implementation, with the proof checked after each change. If an optimization broke the guarantee, the change could not be accepted until the proof worked again. The agents could try different approaches without requiring a human to inspect every implementation in detail.
The results are promising. In one published benchmark, lean-zip compressed a 212 MB collection of test files in 4.57 seconds, compared with 5.77 seconds for a Rust implementation. Other highly optimized libraries remained faster, and lean-zip used more memory. Still, the performance improvements came from a series of changes largely carried out by AI agents.
There are two different checks at work here. The proof establishes that the specified behavior is preserved. Benchmarks measure whether the new implementation is actually faster or more efficient. A version can pass the proof without improving performance, or improve performance while failing the proof.
Combining the two creates an interesting development process. AI can explore many possible implementations, automatically reject those that violate established properties, and keep the improvements that perform better. Leo described proofs as guardrails that allow AI to attempt optimizations engineers might otherwise hesitate to make.
Start by Finding Bugs
Most engineering teams are not ready to formally verify entire applications, and I wouldn’t suggest starting there. An easier entry point is to use AI-assisted formal methods to find bugs in existing software.
Leo also mentioned an experiment by Boris Cherny, who leads Claude Code at Anthropic. Cherny asked Claude to apply formal verification tools to the Claude Agent SDK, software that developers use to build applications with Claude. He reported that a few prompts produced 16 proposed code changes addressing bugs and race conditions. Race conditions occur when a program behaves incorrectly because operations happen in an unexpected order.
That doesn’t mean the entire SDK was proven correct. But it demonstrates that formal methods can deliver value before teams invest in comprehensive proofs. Testing and bug-finding remain useful starting points. As teams identify important properties, they can gradually add stronger guarantees and make those checks part of ordinary development.
What Changes for Engineering Teams
Formal verification has traditionally been expensive because writing proofs required specialized expertise and substantial time. AI is beginning to reduce that burden. As Leo explained, the emphasis may shift toward specifying what software should do and reviewing whether those specifications capture what people actually want.
A specification is a precise description of a program’s required behavior. For a payment system, it might say that money cannot disappear during a transfer or that a transaction cannot be charged twice. Once these properties are expressed precisely, they can potentially be checked whenever the implementation changes.
This could also change how teams maintain software. Requirements documents and architecture diagrams often drift out of sync with the code. Formal specifications can become part of a development process that checks whether implementations continue to satisfy them. They may become increasingly valuable assets as AI takes over more routine coding.
This is extending beyond experimental projects. Microsoft researchers are using AI, Lean, and a tool called Aeneas to verify parts of SymCrypt, its cryptographic software library. Aeneas translates Rust code into a form that Lean can analyze. AI helps construct proofs, while experts remain responsible for important specifications and assumptions.
The broader implication is that engineers may spend less time reviewing routine implementation changes and more time deciding which properties matter, defining acceptable tradeoffs, and checking whether the resulting software behaves as intended.
Where I Would Start
I wouldn’t generalize too quickly from these examples. A proof establishes only the properties that were specified. It cannot guarantee that the requirements were complete or that an AI-generated representation faithfully captures the deployed software. Assumptions about the operating environment can also be wrong. A formally verified compression library might preserve data perfectly while still having security vulnerabilities or performance problems.
The economics are not yet settled either. AI may reduce the labor involved in creating proofs, but writing good specifications, maintaining them, and integrating verification into existing development workflows still takes effort.
I would start with a component whose essential behavior is relatively easy to describe, where mistakes are expensive, and where performance improvements have measurable value. Compression, cryptography, and certain database operations are promising examples. Begin with conventional tests, identify properties worth proving, and experiment with letting AI optimize within those constraints. Measure the entire process, including verification costs and human review.
The opportunity is not to eliminate engineering judgment. It is to use machine-checked guarantees to reduce the amount of routine review needed for certain kinds of changes. If that becomes practical, verification could shift from something that slows development down to something that allows teams to experiment much more aggressively.
Most agent benchmarks tell us whether an agent can complete a task, but not whether it gets better through experience. When problems appear only once, it’s hard to tell whether an agent has learned a reusable skill. Continual-ARC addresses this gap by bringing back the same types of reasoning puzzles with different inputs, charging for examples and wrong answers, and comparing each system with a version reset between jobs. The results revealed that agents left to manage their own memory showed no measurable benefit. Saving tested programs helped on familiar problems, but only training the model improved performance on unfamiliar ones. I’ve argued that your AI should be better on day 500 than on day one. For teams building agents, the challenge is proving that improvement, not just adding memory features.
Ben Lorica edits Ethics.dev and the Gradient Flow newsletter, and he hosts the Data Exchange podcast. He helps organize the AI Conference and the Agent Conference. You can follow him on Linkedin, X, Mastodon, Reddit, Bluesky, YouTube, or TikTok. This newsletter is produced by Gradient Flow.