What does “verified memory safe” even mean?

Large-scale verification breakthrough

On 22 October 2026, Anthropic and Theorem announced that they had used AI to generate proofs for programs built from many open-source libraries.

For readers unfamiliar with the background, there are two reasons this announcement deserves attention.

First, AI is making it easier to find security bugs. This makes the search for ways to secure our software more urgent. Formal methods have long offered a promising approach. They use mathematics to reason about software. Formal verification is one part of this field: we state requirements precisely and prove that a program meets them. Such proofs can establish that entire classes of bugs are absent.

Second, making formal verification scale has long been difficult. There are fundamental limits to what can be automated, and real software is complex. Researchers have spent decades developing techniques to tackle these difficulties, and successful projects have required years of expert effort. The CompCert compiler’s correctness proof, for example, required about six person-years of work. The IronFleet project reported roughly four person-years to develop its methods and build and verify two distributed systems.

This helps explain why producing proofs for much more software, much faster, would be a major advance.

Methodology used in the breakthrough

Let us now look more closely at what Anthropic and Theorem actually proved. This will make our concerns easier to understand.

The team wanted to address memory-safety bugs, a major source of security vulnerabilities.¹ For this, they turned to AddressSanitizer (ASan), a widely used tool for detecting memory-safety bugs.

What does this mean for security?

At this point, it is imperative to ask: how should we understand what they have achieved? Have Anthropic and Theorem solved cybersecurity? Have they solved memory safety? We don’t think so.

This distinction will be familiar to many Computer Science researchers, especially those working in software security, formal verification and programming languages. Researchers have long discussed what memory safety means and clarified the guarantees that different tools provide.³ We explain the distinction here for readers who may not have considered it carefully.

ASan is an effective bug finder. Its original paper already reported hundreds of previously unknown bugs found in Chromium and other software.⁴ But ASan also misses memory-safety bugs—even when the faulty memory access actually happens.⁵ Proving that a program never triggers an ASan error therefore does not establish that it is memory safe.

The examples below explain this gap, including how it arises in OpenSSL. In our paper, we discuss the technical details in depth.

So here is the takeaway in one line:

The blog post does acknowledge this issue as part of its broader discussion of limitations. It says:

However, ASan doesn’t detect all memory safety bugs…

But this message may get lost when different limitations are clubbed together as gaps that will be easily closed in the near future. Not all disclaimers are equal. The proofs could be extended to other processors. But that would not solve memory safety. We first need to acknowledge that memory safety is a larger problem. It requires careful thinking about specifications. Producing proofs faster, or for more programs, does not by itself solve a problem on which the security of today’s infrastructure depends.

The harder problem: getting the specification right

At a high level, the message is simple: if you do not know what you are proving, you may end up proving something useless. For experts in formal verification, this has always been clear. The specification you check your program against must capture your actual intent.

As an example, we already know stronger specifications for memory safety than “ASan safety.” These account for individual objects, their boundaries and their lifetimes. (SoK: Sanitizing for Security) Our technical report examines these distinctions in the specifications used in this project.

Faster proofs do not tell us whether we chose the right requirement. Specifications deserve extra scrutiny. This is especially so when an AI is rewarded for producing an accepted proof. If the specification is too weak, the AI may find a shortcut that earns the reward while defeating the original intent. This is the risk of reward hacking: satisfying the formal target without achieving what we actually wanted.

Why getting the specification right is hard

Why is getting the specification right so hard? What even makes a good specification? At the very minimum, it must be understandable to people. A user should be able to tell what “I proved this program correct against this specification” actually guarantees. It must also be precise enough for a mathematical proof. But above all, it must capture what we actually intend. That is the hard part.

Sometimes, programming language features and types help express that intent. For example, an array type can make a buffer’s bounds explicit. Rust’s lifetime annotations let programmers express relationships between how long references remain valid.⁶ These and other features make Rust an attractive choice for writing memory-safe software. Many researchers are now developing ways to translate existing C software to safe Rust automatically.⁷ But programs can also manage their own logical objects, as in OpenSSL’s pool of temporary numbers. The memory can stay allocated even after a temporary should no longer be used. To specify that rule, we need to understand how the programmer intended the pool to work.

Sometimes, though, we do not yet know what the specification should say. We may discover new requirements years after the software has been deployed. Worse still, we may discover them only after the software fails in production or an attacker exploits a vulnerability. This also makes automatic specification inference hard. Inferring what the code does is different from deciding what it should do.

One thing is clear: with the technology we have right now, it is imperative to involve human judgement in choosing and reviewing specifications. Automating this task would require reliable ways to discover the right requirements and assess whether they capture the intended guarantees. Producing proofs at greater speed and scale is a substantial advance. But its value for security still depends on whether we are proving the right thing.