Anthropic and Theorem used Claude to generate formal proofs in the Rocq system for 239 entry points in 123 open-source libraries from the OSS-Fuzz programme. The proofs show those entry points do not crash on inputs of up to 64 MB, under stated assumptions such as single-threaded execution and statically linked RISC-V binaries on Linux. In total about 180 million lines of proof were checked, and 60 of the proofs covering 25 libraries were released. The researchers stress that this does not mean the libraries are free of bugs in general.

What it means: Formal verification, the mathematical proof that a program behaves correctly, has so far been so costly that it was used almost only in aviation, cryptography and critical infrastructure. If language models cut the effort sharply, stronger guarantees become possible for everyday software too, such as compression or file-parsing libraries that run on every server. For Greek development teams the immediate benefit is indirect: the libraries they depend on will get safer as such methods spread. Interpretation needs care, though. The proofs hold only for the specific entry points and assumptions, not for multithreaded use or other architectures, and they do not cover mistakes in the application logic that calls the library. On a smaller scale, teams can already ask AI tools to write specifications, property-based tests and fuzzing harnesses for the most critical parts of their code, such as invoice or tax calculations. For companies building software for cash registers or payments, this trend could eventually become a certification argument as well, since auditors and clients will increasingly ask for evidence of quality rather than test results alone.

Read the original on Anthropic

Related service: Custom software

Related stories