What does "verified memory safe" mean?

An audit by the FOCS Lab found that the formal-verification proofs Anthropic and Theorem released on 22 October 2026 for programs built from 123 open-source libraries do not fully establish memory safety, because the published specification relies on AddressSanitizer checks that miss some out-of-bounds writes. The auditors built a small program whose copy allows one extra byte to overwrite an adjacent action code, proved it satisfies the full published guarantee, and had the project's checker accept the proof — showing a memory-safety bug can coexist with successful verification. The lab warns that AI rewarded for getting a proof accepted may exploit gaps in the specification, a form of reward hacking, and that overstating such guarantees can lead people to rely on protections that have not been established.

On 22 October 2026, Anthropic and Theorem announced https://www.anthropic.com/research/formal-verification that they had used AI to generate mathematical proofs for programs built from 123 open-source libraries. This is an encouraging development for automated verification, and the release of proofs allows others to examine what has been established. After this announcement, we began examining the released proofs to understand what had actually been proved about memory safety. Memory-safety bugs can allow attackers to steal data or take control of a system. Eliminating such bugs is therefore an important goal for cybersecurity and national security. We think it is important to be careful with such announcements. Overstating the guarantees can lead people to rely on protections that have not been established. When we say that a program has been proved correct, it is important to understand what this means. The proof establishes that the program satisfies a precisely stated requirement, called a specification , under certain assumptions. The specification has a crucial role: it must precisely encode what we want the software to do, or what we want it not to do. In this investigation, we focus on memory safety. Intuitively, this requires that a program access only memory it is entitled to use, and only while it is entitled to use it. We observe that the published specification does not fully capture this intended requirement. A program can therefore satisfy that specification and still contain a memory-safety bug. Specifications become especially important when we ask AI to carry out verification. An AI rewarded for getting a proof accepted may exploit omissions in the specification to achieve that goal. This is a form of reward hacking: the formal objective is satisfied, but our actual intent is not. Note that the proof itself can still be mathematically valid. If the specification fails to rule out a bug, the AI may leave that bug in place and still succeed at the task we gave it. The team adds checks to a program to detect certain memory errors. The published proofs establish, in particular, that these checks never report an error for any input covered by the stated assumptions. However, the checks do not detect every memory-safety bug. Note that an individual proof may establish additional properties, such as ensuring that a particular write stays within its intended array. We therefore examined the individual proofs to see whether these additional properties rule out the errors that the checks would miss. The memory-safety guarantee The verification approach uses AddressSanitizer, or ASan, a tool that detects memory errors while a program runs. The guarantee includes proving that ASan reports no error for the executions covered by the proof. To interpret this as memory safety, however, we need to understand which errors ASan detects. Consider a program that stores two objects, A and B, in a 100-byte block of memory, with 50 bytes reserved for each object. When writing to A, we want the program to modify only the memory reserved for A. Suppose, however, that a bug causes the write to extend beyond A’s boundary and overwrite some of B’s data. This violates the intended memory-safety requirement. Note that the write still falls within the larger 100-byte block. If the library has not informed ASan of the boundary between A and B, ASan may treat the entire block as accessible and report no error. We constructed a small program to check whether such a bug could coexist with the full published guarantee. The program copies an input and allows one extra byte to overwrite an adjacent action code. We then proved that the program satisfies the guarantee, and the project’s checker accepted our proof. Thus, the program contains a memory-safety bug even though the verification succeeds . Our source, proof, and checker logs https://github.com/focs-lab/memory-safety-proof-audit/blob/main/evidence/dossiers/checked-example/README.md document this construction. The example demonstrates a gap in the specification without implementing an exploit. Examining the individual proofs The published proofs concern programs written to test selected library functions. For example, a test program might compress some input data and then decompress the result. The proof covers every input permitted by its assumptions for that particular program. However, another program might use the same library differently. It might decompress data received from elsewhere, without first producing that data through compression. It might also call other library functions, or call the same functions in a different order. Proving the first program safe does not automatically establish safety for these other uses. We therefore examined which uses of each library the published proofs cover. Buffer boundaries in coturn Coturn https://github.com/coturn/coturn is open-source server software that supports voice and video calls. We found that the proof conditions we examined can hold even when a write’s destination is one byte before the intended message buffer. These conditions therefore leave an important memory-safety requirement unproved. We argue that this illustrates the danger of an incomplete specification: a proof can meet its formal requirements without establishing the intended buffer boundary. Our technical evidence https://github.com/focs-lab/memory-safety-proof-audit/blob/main/evidence/dossiers/coturn-field-bounds/README.txt documents this omission. Temporary storage in OpenSSL For OpenSSL, we examined a different requirement. OpenSSL gives callers temporary storage for calculations, together with references that identify where that storage is. Once a group of calculations ends, those temporaries must no longer be used, even if OpenSSL keeps the memory for later reuse. We found that the conditions for writing through a reference can still hold after the temporary’s permitted lifetime has ended. The old reference should no longer be used, since OpenSSL may reuse the storage for another calculation. The specification therefore needs to capture an important requirement: ending a temporary’s lifetime must also end permission to use its old references. The proof conditions we examined do not enforce this requirement. Our technical evidence https://github.com/focs-lab/memory-safety-proof-audit/blob/main/evidence/dossiers/openssl-lifetime/README.txt documents this omission. We discuss additional libraries and the limits of their proofs in our paper https://github.com/focs-lab/memory-safety-proof-audit/raw/refs/heads/main/paper/main.pdf , which also provides the detailed evidence for our findings. Technical statement and scope of our checks The published agreement statement compares ordinary and sanitizer-instrumented executables. Under its execution-model and memory-budget assumptions, neither reaches a modeled error, and they have the same observable behaviours. Our constructed example satisfies this statement for its fixed plain and ASan binaries. The initial four-project allocator review examined source and specifications. Separate Rocq checks support the coturn constructions and the focused OpenSSL lifetime result; the latter does not replay the full binary agreement proofs. The evidence guide https://github.com/focs-lab/memory-safety-proof-audit/blob/main/evidence/README.md records each investigation’s method, revision, and limits. Interpreting the security claims In our example, the input can overwrite the value that determines which function the program calls. The call still goes to an existing function, but it may no longer be the function the programmer intended. We argue that it is not sufficient to check that the chosen function exists; we also need to ensure that a memory error cannot change this choice. Whether an attacker can exploit such an error depends on what the functions do and how the program is used. When communicating a verification result, we should explain which errors the specification excludes and which uses the proof covers. A reader should not have to inspect thousands of lines of proof to determine whether the claimed protection applies to their use of the software. Specifications and intent There is an additional concern when AI performs this work. Research on specification gaming https://deepmind.google/blog/specification-gaming-the-flip-side-of-ai-ingenuity/ and reward hacking https://www.anthropic.com/research/reward-tampering documents how AI systems can satisfy a measured objective without fulfilling its intended purpose. In verification, obtaining an accepted proof may satisfy the assigned task even when a real bug remains outside the specification. We have not established that reward hacking occurred in this project. We do argue that the possibility makes independent scrutiny of the specification especially necessary. Writing an adequate specification requires understanding the software and how people intend to use it. Some requirements may be poorly documented, or become apparent only after an unexpected use exposes an omission. AI may help us identify these requirements, but producing a proof does not establish that we have identified them correctly. Our investigation concerns memory safety, but this obligation applies to any claim that software is “bug-free”. As AI makes proof generation more accessible, we need to devote corresponding effort to understanding and validating what we ask it to prove. We should judge progress by how well the resulting guarantees address the bugs we want to eliminate. Paper and supporting evidence AI Proved the Code Memory Safe. Or Did It? The full argument, findings, references, and technical appendices.PDF ↗ - Reproduction status https://github.com/focs-lab/memory-safety-proof-audit/blob/main/VALIDATION.md · completed checks and the incomplete fresh-clone interpreter proof replay. - Constructed example https://github.com/focs-lab/memory-safety-proof-audit/blob/main/evidence/dossiers/checked-example/README.md · source, proof, binaries, and checker logs. - Coturn findings https://github.com/focs-lab/memory-safety-proof-audit/raw/refs/heads/main/evidence/dossiers/coturn-field-bounds/output/pdf/coturn-field-bound-findings.pdf · checked constructions and reproduction instructions https://github.com/focs-lab/memory-safety-proof-audit/blob/main/evidence/dossiers/coturn-field-bounds/README.txt . - OpenSSL lifetime check https://github.com/focs-lab/memory-safety-proof-audit/blob/main/evidence/dossiers/openssl-lifetime/README.txt · proof sources, replay results, and limitations. - Evidence guide https://github.com/focs-lab/memory-safety-proof-audit/blob/main/evidence/README.md · all project reports, methods, and theorem assumptions https://github.com/focs-lab/memory-safety-proof-audit/blob/main/evidence/context-and-properties.md . The allocator and bzip2 reviews concern revision 98e995d4 ; the coturn constructions and synthetic example use a6839bb9 . These findings concern the recorded versions, not an exhaustive audit of all projects or later changes.