Imagine being able to prove, with the same intellectual certainty as a mathematical theorem, that a piece of software will never leak a password, scramble a message, or leave a door open for an attacker. This is the promise of formal verification, a discipline that has existed for decades but is now being transformed by artificial intelligence. Formal verification is not ordinary testing. It is a kind of mathematical audit: a machine reads a program, compares it with a precise description of what the program is supposed to do, and generates a proof, in a language that machines themselves can check, that the program and the description match. Earlier this year, Apple’s security team gave a striking endorsement of the technique. Some of the issues uncovered by formal verification in its corecrypto library, the code that handles encryption across millions of Apple devices, could not have been found any other way, the team said. That is a notable admission from a company known for its secrecy and its confidence in its own systems. Encryption libraries are especially demanding: a tiny mistake can defeat the strongest cryptography, but the mistake may be invisible to ordinary testing because it only appears under unusual mathematical conditions. Apple’s words suggest that verification is emerging as an essential safety net, not an academic luxury. Yet the company also warned that the technique is not easy to scale. Apple said it has to be conservative when adding new code to corecrypto, making sure that its verification and review work can keep pace. That captures the central tension of the entire field: formal verification is powerful, but it is also time-consuming, expensive, and hard to deploy widely, and even a company with Apple’s resources must plan carefully before changing code that millions of people depend on. The challenge now, as artificial intelligence reshapes software development, is whether AI can make verification fast and practical enough to become a normal part of how all software is built, rather than a rare luxury reserved for the most critical lines of code.
For all that enthusiasm, formal verification still strikes many people in the technology industry as a costly, slow, and somewhat exotic discipline. It can require a team of specialists, years of mathematical training, and a great deal of patience. Two cybersecurity executives at major companies, both of whom were not allowed to speak publicly, say they are still waiting to see whether automation will change that calculation. Their companies have not formally verified any of their code. They do not dispute the value of finding security flaws before attackers do, but they are not yet convinced that the cost of introducing formal-verification tools into their engineering pipelines will pay for itself. In the current environment, every engineering dollar is scrutinized, and security spending in particular needs to be justified in terms of risks, deadlines, and revenue. The executives said they could imagine a future in which the calculus changes, but not necessarily by building their own verification teams. Instead, they could see themselves paying major AI labs, companies like Anthropic or its rivals, to supply so-called verified AI-generated code. The idea sounds like a blend of two very different promises: the speed and creativity of generative AI, combined with the mathematical certainty of formal proof. From a business perspective, it is attractive. It would let companies buy security as a service, rather than investing years in building a rare and expensive capability on their own. It would also place enormous responsibility on the AI labs, which would essentially be certifying that the code they sell or license is not only useful but mathematically guaranteed to behave as advertised. That is a heavy burden, and it is not clear whether any AI company is ready to accept it. But the very fact that experienced security executives can imagine it is a sign of how fast the conversation around verification is moving.
Open source software projects, which form the foundation of many applications, are already moving into this unfamiliar territory. The nonprofit Beneficial AI Foundation used grant money from Anthropic this year to validate the same encryption code that a Stanford researcher had previously verified in an academic exercise. This matters because encryption libraries are not only used by technology giants; they appear everywhere, from banking apps to messaging services, often embedded in open source components that few people ever read. The code in question, known as curve25519-dalek, is a library for modern elliptic-curve cryptography, and its maintainers are volunteers or people working with very little funding. One of those maintainers, Michael Rosenberg, says he hopes that sustainable funding will eventually emerge for ongoing verification efforts. But he is not optimistic about the mechanics. “I have no ideas as to how that’s going to happen, though,” he says, “and we certainly shouldn’t rely on the goodwill of the AI companies.” His words capture a fear shared by many open source developers: the same companies experimenting with AI to improve verification are the ones who own the AI models, and their incentives may not always align with the public interest. If an AI company pays for verification of an open source library, it might be doing so to demonstrate its own technology, or to create goodwill, but not necessarily to maintain the library for years. Open source maintainers are already chronically underfunded, and the addition of formal verification, which requires specialized expertise, only makes the financial gap wider. Yet the experimentation is real, and the early results are encouraging. Verification tools powered or assisted by AI are beginning to reduce the amount of tedium involved in proving code correct, and open source projects are natural testing grounds because their code is visible, their collaborators are geographically dispersed, and their users depend on a fragile ecosystem of volunteers. The question is who will ultimately pay for the common infrastructure on which the entire industry relies.
A number of startups are hoping to turn this promise into a business. They are not all sure, however, whether to sell their tools directly to software developers or through intermediaries, especially major AI labs like Anthropic. Their general strategy is to use AI to automate what is often the hardest part of formal verification: deciding what a program is supposed to do. In formal verification, every claim about a piece of code must be spelled out in advance. The specifications operate like contracts. For a data table, for example, a developer might require that the table contain exactly the same items before and after a sorting operation, merely in a different order. It sounds simple, but writing such specifications for real-world software is laborious. This is where AI enters the picture. AI systems can read code, infer behavior, and propose specifications that human experts can then review. Once the specifications exist, another set of automated techniques, which may not involve AI at all, translates the code and the specification into a format that mathematical proof tools such as Lean, Rocq, and Isabelle can understand. Those tools are the workhorses of modern formal verification. They are not simply running the code; they are constructing and checking formal arguments, line by line, about why the code satisfies its specifications. The combination of AI for generating intuition and math checkers for verifying the details is intoxicating to many researchers. It could finally make verification practical for ordinary software, not just for safety-critical systems like aircraft controls or cryptographic primitives. But this is also where the entrepreneurial uncertainty begins. If the AI-generated specifications are wrong, or too vague, or written in a way that hides the developer’s intent, the entire proof might be valid and yet useless, proving that the code meets the wrong requirements. That concern has led some startups to consider working closely with AI labs, which control the models and the distribution channels, while others want to build direct relationships with engineering teams. The startup world is still deciding whether formal verification will be a feature inside a larger AI platform or a standalone service sold to developers who care enough about security and correctness to pay for it.
One of the newest entrants to the field is Madan Musuvathi, a veteran of Microsoft Research who left after more than two decades to found a startup called Truidic. Musuvathi has spent much of his career studying how systems software behaves and how to prove it correct. His decision to commercialize this work was driven in part by a growing sense that the security world is entering a dangerous new phase. After high-profile incidents involving AI systems and platforms such as the OpenAI hack and the breach at Hugging Face, he felt there was an urgent need to take verification out of the lab and into the market. His warning is direct: “AI in the hands of attackers can be extremely powerful,” he says, and verification can “make AI safe and secure for everyone, everywhere.” That phrasing may sound idealistic, but it reflects a real shift. Traditional security tools often focus on monitoring, patching, and reacting to attacks. Formal verification, in contrast, aims to eliminate entire classes of bugs before they ever become vulnerabilities. Musuvathi’s bet is that companies will recognize this difference and pay for products that provide mathematical guarantees, not just high hopes. The urgency comes from the fact that AI is now being used to write code at massive scale, and much of that code is not being subjected to the kind of scrutiny that security experts recommend. If AI programmers produce more code, they also produce more bugs, and if attackers can use AI to find those bugs faster than defenders can fix them, the situation will spiral. Verification offers a way to slow that spiral. It does not promise that software will be perfect, only that its behavior is mathematically aligned with a stated set of specifications. But in a world where an attacker only needs one mistake, even that limited promise is valuable. Musuvathi is not alone in thinking that the commercialization of formal verification is not just a business opportunity but a public-safety measure.
For Proofcraft, one of the few companies that has offered traditional formal verification for years, the new attention is both exciting and slightly uncomfortable. The company, led by CEO June Andronick and chief scientist Gerwin Klein, says the growing excitement about verification is translating into a flood of incoming requests. Interest is so strong, they say, that it easily outpaces what Proofcraft and all its competitors are able to provide. That is a good problem to have, but it comes with risks. Andronick and Klein worry that the recent enthusiasm for AI-generated specifications may inspire what Klein calls “unjustified trust” in the final results. Just because a proof is correct does not mean the specification is correct. A specification is still a human product, and if it is produced by a large language model, it may be fluent, confident, and wrong. The math tools will dutifully prove that the code satisfies the specification, and everyone will feel good. But if the specification did not truly capture the intent of the user, the proof is an illusion. The two leaders want the verification community to hold on to a culture of skepticism and rigor, even as it welcomes new tools and new sources of funding. They also want to preserve something less tangible: the set of intellectual pleasures that keep people in this field passionate. Klein describes formal verification as “pretty addictive, like a puzzle game.” There is a particular joy in taking a tangled, messy piece of code and reducing it to a crisp mathematical argument, then checking every step until the proof clicks into place. If the current wave of interest goes well, Klein will have more opportunities to do that than ever. The future of formal verification, after all, is not just about AI, markets, and security. It is also about a community of deeply engaged people who believe that software can be made better, safer, and more honest, and who are willing to do the painstaking work to prove it. That spirit, perhaps more than any particular technology, is the reason the field has survived long enough to have this moment.
