Anthropic published research, done with formal-methods firm Theorem, in which Claude wrote proofs over compiled RISC-V assembly for 123 real-world open-source libraries. The proved property is narrow but strong: for every input under 64 MB, and every modelled Linux response and memory layout, each program always exits normally without a memory-safety error or failed assertion - assuming it runs as a single-threaded static binary with a fixed memory budget on a RISC-V CPU. Anthropic calls it, to its knowledge, the first large-scale application of AI to formal verification of production software at the assembly level, and says Claude found bugs that had survived trillions of test executions. A subset of the proofs, plus the RISC-V and operating-system semantics they rest on, were released; Theorem is publishing a Claude skill and offering to run the same pipeline on other projects. Anthropic also describes side experiments, including a security assessment of zlib and a proof of behavioural equivalence for a Python interpreter written in Rust.
Our takeThe scope assumptions do almost all the work: single-threaded, static, fixed memory budget, modelled OS responses. Proofs of that shape say nothing about concurrency, dynamic allocation or adversarial timing, which is where most exploitable memory bugs live. The bug-discovery claim also needs the disclosed list to be judged, since 'eluded trillions of runs' is not the same as 'was reachable in production'. The reusable asset is the published semantics and proof subset, which is what should make the next project cheaper than the last.