Vulnerabilities discovered in six libraries already reviewed by Anthropic’s AI

GenProof discovered bugs in six libraries examined by Anthropic and launches QuickProof to make formal verification more accessible.

A mathematical proof can be perfectly correct and still let a bug slip through. That is the paradox highlighted by GenProof, a new research lab specializing in formal software verification. Its researchers say they have discovered errors in six open-source libraries, some of whose properties had already been proved by Claude, as part of a program led by Anthropic and Theorem. The earlier proofs would not be wrong: they would simply have checked insufficient properties to detect the errors found.

Founded in particular by Alex Pokras, the lab is launching two tools, QuickProof and QuickMaths. The first aims to make formal verification accessible to developers without any particular math expertise. The second coordinates several AI agents to solve proof problems in Lean. According to the public discoveries registry, the lab’s research covers 111 projects and totals 352 identified bugs, including 134 fixed and 212 that were the subject of public reports. These figures correspond to the state of the registry as communicated at launch and include issues of widely varying severity. A correct proof can verify the wrong thing

Formal verification consists in mathematically proving that a program satisfies a precise property, for all inputs allowed by that property. Unlike conventional tests, which examine a limited number of situations, a proof can cover an entire set of behaviors defined by its specification.

The problem lies precisely in that specification. Proving that software never crashes does not guarantee that it returns the right result. A compression function can produce an incorrect file without causing a runtime error. A computing library can return an erroneous value while still respecting the memory-safety constraints imposed on it.

On October 22, Anthropic and Theorem published the results of a program in which Claude had proved safety properties on 239 entry points belonging to 123 open-source libraries. The researchers had worked directly on RISC-V executables, with around 180 million lines of proofs checked by Rocq, a formal proof assistant.

The approach mainly aimed to establish that certain programs could not crash under the conditions defined by the tests used as specifications. The authors themselves acknowledged that these guarantees covered neither all the libraries’ features nor all their runtime environments.

The GenProof team revisited six libraries included in that publication: zstd, OpenSSL, libpcap, zlib, Mbed TLS, and coturn. Errors were identified in each of them, without invalidating the earlier proofs. The published analysis highlights a fundamental difference between proving that a program runs without incident and demonstrating that it performs the intended task correctly. Bugs in Redis, Linux, and historic libraries

One of the most documented findings concerns Redis, a software package widely used to store and manipulate data in memory. A change introduced in version 8.8 modified how certain input sizes are handled in the internal listpack format.

This change could make previously valid data, saved with Redis 8.6 or an earlier version, unreadable. Under certain conditions, a simple read after an upgrade caused the server to stop. With particular settings, entries could become invisible and then be saved as duplicates. The issue was the subject of Redis report no. 16078, followed by a fix.

Conventional tests did not necessarily detect this incompatibility, since they generally checked that a given version could reread the data it had just written. By examining all representations allowed by the format specification, the researchers identified three particular sizes that caused the malfunction.

Other investigations focused on the Linux kernel. The lab says it discovered an old flaw, potentially remotely exploitable to cause a vulnerable device to crash, in a component that Anthropic and Theorem had previously studied. A CVE identifier request was submitted, but the registry consulted does not yet provide an assigned reference. The exact scope of this vulnerability should therefore still be regarded as the lab’s claim, pending the corresponding technical elements and public validations.

The work also concerns widely used components such as zlib, OpenSSL, nginx, and data-processing libraries. Some reports have already been fixed by the project maintainers; others remain under confirmation or review. The detailed investigations published by GenProof distinguish ordinary functional errors from vulnerabilities that may have security consequences. Writing a C test to obtain a mathematical proof

One of formal verification’s main difficulties lies in writing specifications that a proof assistant can understand. Traditionally, this step requires mastery of specialized languages, which limits adoption in mainstream development teams.

With QuickProof, GenProof offers an interface based on the C language. The developer describes the expected property in a small program that looks like a unit test. For a compression library, they can ask that the data obtained after compression and then decompression be identical to the original data.

The difference lies in how the inputs are defined. Instead of testing a few chosen files, the developer indicates the authorized categories of data, then asks that the property hold for all of those possibilities. In a published example, the exercise covers all byte sequences whose size does not exceed 4 KiB.

The software then transforms this description into a theorem usable by Rocq, using Verified Software Toolchain, a verification environment developed at Princeton for C programs. AI agents write the proofs, while an independent checker verifies their validity.

The specification is fixed before proof work begins. The agents can modify only the proof files, which prevents them from silently simplifying the property to be proved in order to obtain a favorable result. A verification command then rebuilds the files from a clean environment and ensures that the