Anthropic uses Claude to formalize and validate 123 open source libraries, discovering vulnerabilities that have been lurking for many years On October 23rd, according to the Anthropic research blog, Anthropic collaborated with Theorem to formally validate 123 open source libraries using Claude at the RISC-V assembly level, proving that under specific assumptions (single threaded static binary, fixed memory budget, RISC-V CPU and Linux system, input less than 64MB), there will be no memory security errors or assertion failures for any input. The relevant proof covers 239 entry points and approximately 180 million lines of Rocq code. Anthropic stated that this is the first large-scale attempt at AI formal validation of production software at the assembly level. During the process, Claude also discovered and patched vulnerabilities that had been lurking for many years and had not been detected even after trillions of test runs. Anthropic also suggests that formal validation does not mean no vulnerabilities, and its conclusions depend on assumptions about trusted components such as RISC-V and Linux semantics.