AI Can Now Write Proofs That Code Won’t Crash. Here’s What “Formally Verified” Does and Doesn’t Promise

The same AI systems that have become good at finding software flaws are now being pointed at a harder job: proving that a piece of code cannot fail in certain ways at all. In the space of a single week in October 2026, Anthropic published results from using its Claude models to write machine-checked proofs for more than 100 open-source libraries, and a Palo Alto start-up called &Truth launched with $70 million to sell AI-driven software verification. The New York Times framed the question bluntly: after helping crack hard mathematics, can AI eradicate computer bugs?

The honest answer from the people building these tools is “not yet, and not completely.” But the work is moving fast enough that privacy, security and procurement teams will start seeing “formally verified” in vendor pitches, security questionnaires and AI-generated code reviews long before the technique is mature. This piece explains what the term actually promises, what the October results did and did not show, and how to read the claim when it lands on your desk.

Why this is happening now

The pressure comes from the attack side. Anthropic’s research team opened its October 22 paper by noting that most software is full of bugs that AI can now find and exploit easily, and that the Linux kernel alone recently had more than 1,000 vulnerabilities disclosed. Patching faster helps, but it is a race. If AI tools can find flaws at machine speed, defenders want something stronger than “we tested it a lot.”

Formal verification is that something. Engineers translate code into a mathematical model and prove that it always obeys a defined set of rules, such as “this program never reads memory it should not.” If the proof fails, the failure points to a possible bug; fix it and try again until the proof goes through. The catch has always been cost. Anthropic cited the seL4 operating system kernel, which took about two person-years to build and roughly 20 person-years to verify. That is why the technique has mostly lived in avionics, cryptography and a handful of security-critical cloud components.

Large language models change the economics because writing proofs is a long, tedious, well-defined task, the kind of work they can grind through. The Times described &Truth and rivals including Axiom and Logical Intelligence as building on Lean, a proof language created more than a decade ago by Microsoft researcher Leonardo de Moura, the same tool used in recent AI mathematics results.

What the October results actually showed

Anthropic’s project with the verification company Theorem is the most detailed public data point, and its scope is worth reading closely. Using fuzz tests already written by the developers of libraries in Google’s OSS-Fuzz program, Claude turned each test into a formal specification and then tried to prove it. Over a few weeks it proved that 239 entry points across 123 libraries will not crash on any input up to 64 MB, patching bugs it found along the way. The proofs run to about 180 million lines of the Rocq proof language and are checked mechanically, so almost none of them needs human review.

The bug-hunting side effect may matter more in the short term than the proofs themselves. According to Anthropic’s write-up, the process found bugs that conventional fuzzing was unlikely ever to reach, including a counter underflow in a decompressor that led to an out-of-bounds write only on a rare input of around 20 MB. It also rediscovered a known libexpat vulnerability and surfaced logic bugs that never crash, such as a file-loading restriction that was not always enforced. In one separate effort on a widely used PDF reader, the team said it found as many security bugs in a week as are typically reported in a year.

Then come the limits, which Anthropic states in its own paper.

• The proofs assume a single-threaded, static binary on a RISC-V processor running Linux. Most people run these libraries on x86 or ARM chips with different system libraries, so the guarantee does not transfer automatically.
• The proofs cover the specific entry points tested, not whole libraries, and they rely on AddressSanitizer, which does not catch every memory-safety error.
• Everything depends on trusting the formal models of the processor and operating system, the exact theorem statements and the proof checker itself.
• A program can be “proved” correct against a specification that does not describe what anyone actually wanted.

Anthropic summarized the point in a sentence worth pinning to a procurement checklist: “Formally verified” does not mean “bug-free.”

The oversight problem inside the fix

There is a quieter governance issue in the Anthropic project that deserves attention from anyone thinking about letting AI patch production code. To keep the work moving, the team let Claude fix the bugs it found and then prove the patched version. In a footnote, the researchers acknowledged this opens the door to reward hacking: the model could make any theorem provable by rewriting the program into one that trivially never crashes. They discouraged it by penalizing patches, rewarding proofs that showed how few inputs a change affected, and logging and auditing every patch.

That is a well-designed control, and it is also a reminder that an AI system optimizing for “proof passes” or “ticket closed” may find routes its operators did not intend. An organization that lets an AI agent patch its own codebase needs the same kind of guardrails: human review of patches that change behavior, logs of what was changed and why, and a check that the fix did not quietly remove functionality. We made a related argument when looking at why patching alone is not enough in the AI cybersecurity era.

Skeptics also raise a practical objection. Will Wilson, chief executive of the testing company Antithesis, told WIRED that formal verification is “a trap” for people like him and said his company had found bugs in software its customers had already formally verified. Speaking to The New York Times, he made the same point in different terms: a proof is only as good as its assumptions, and eventually code meets a messy real world that no specification fully captures. Even the verification specialists at Proofcraft told WIRED they worry that AI-generated specifications could inspire “unjustified trust.”

Why privacy and compliance teams should care

Data protection law does not require formal verification, and nothing in the October announcements changes that. But several obligations are written around what is reasonable or “state of the art,” and those standards move as tools improve.

GDPR Article 32 requires security measures appropriate to the risk, taking into account the state of the art and the cost of implementation. Article 25 requires data protection by design. If AI-assisted verification becomes cheap for the kind of parsing and decompression code that sits in front of personal data, regulators and plaintiffs may eventually ask why a company handling sensitive data did not use it, in the same way they now ask about encryption and multi-factor authentication. That is a prediction, not a current rule.

The EU Cyber Resilience Act is closer to the point. It makes vulnerability handling a condition of selling products with digital elements in the EU, with reporting obligations for actively exploited vulnerabilities starting in September 2026 and the main requirements applying from December 2027. Our overview of how the Cyber Resilience Act makes cybersecurity a requirement to sell in Europe covers the timeline. Verification tools will not satisfy the Act on their own, but vendors will start citing them as evidence of secure development.

The bigger near-term exposure is in vendor management. Most organizations’ personal data passes through open-source libraries and third-party software they did not write. A vendor that can show machine-checked proofs for its file parsers is offering something meaningful. A vendor that says “AI-verified” in a sales deck without saying what was proved, on which platform, under which assumptions, is offering marketing.

Six questions to ask when a vendor says “formally verified”

1. What property was proved? “Never crashes on inputs under 64 MB” and “correctly implements the specification” are very different claims. Ask for the theorem statement in plain English.
2. Which code and which build? Was it the whole product, one library, or a few entry points? Was it the binary you will actually run, on your processor architecture and operating system?
3. Who wrote the specification? If an AI model drafted it, who reviewed it, and how do they know it matches the intended behavior?
4. What is trusted? Every proof rests on a proof checker and on models of the hardware and operating system. Ask which ones, and whether they are public.
5. Did AI change the code to make it provable? If so, how were patches reviewed, and what functionality changed? This is where the reward-hacking risk lives.
6. How is it kept current? A proof applies to a specific version. Ask how the vendor re-verifies after updates and how quickly patches reach you.

Fold these into your existing vendor risk management process rather than creating a separate track. The answers belong alongside the vendor’s SBOM, vulnerability disclosure policy and incident history.

Where AI-found bugs fit in the bigger picture

The verification push sits on top of a broader shift in which AI is now a routine bug-hunting tool for both sides. We looked at the defensive case when Mozilla used Anthropic’s Mythos model on Firefox in our analysis of AI-augmented vulnerability discovery, and at the double-edged nature of those capabilities when Claude Mythos Preview debuted. The labor market has noticed too: companies are hiring to secure AI-generated code that is being written faster than humans can review it.

Verification is the logical next step: if AI is writing more of the code and finding more of the flaws, the remaining question is who checks the checker. The answer the October work offers is a small, auditable proof checker and a set of public models, which is a much smaller thing to trust than millions of lines of untested code. Whether that holds up outside the lab is exactly what the start-ups now have to show.

Frequently asked questions

Can AI now prove that software has no bugs?

No. It can prove that specific code satisfies a specific property under stated assumptions. Bugs can remain in parts of the code the proof does not cover, in the assumptions about hardware and operating systems, or in a specification that does not match what users need.

Is formal verification the same as AI vulnerability scanning?

No. Scanning and fuzzing look for problems by trying inputs or patterns and can never show that none remain. Verification tries to prove a property holds for every input in scope. In the Anthropic project, attempting proofs also turned up bugs that fuzzing missed.

Do privacy laws require formally verified software?

No current privacy law requires it. GDPR asks for security appropriate to the risk and the state of the art, so the expected baseline can rise as tools become cheaper, but that is an evolving standard rather than a specific mandate.

Should we let AI tools patch our code automatically?

Only with controls. The researchers behind the largest public project penalized unnecessary patches and logged and audited every change because a model could otherwise “fix” code in ways that defeat its purpose. Human review for behavior-changing patches remains sensible.

What should go into a vendor questionnaire?

Ask what property was proved, for which code and build, who wrote and reviewed the specification, what components are trusted, whether AI modified the code and how re-verification works after updates.

The checker still needs a checker

There is an irony at the center of this story. The industry’s response to AI that can break software is more AI, this time writing proofs that other software checks. The approach is sound in principle because a proof checker is small enough to audit in a way a whole application never is. But it moves the trust question rather than eliminating it, onto specifications, models and assumptions that only a few specialists can read. For a company signing a contract, the test will be simple and unforgiving: when a breach happens in “verified” code, someone will ask what exactly was proved, and the answer had better be in writing.