AI Makes Mathematical Proof of Secure Code Practical at Scale

Anthropic reports that most software contains bugs, and AI can now find and exploit them with ease. Its researchers argue that standard defences are no longer enough, and that developers need ways to prove code is free of certain flaws. Formal verification offers that guarantee, but it has historically needed years of expert effort, which made it impractical for most real-world projects.

In a collaboration with Theorem, Anthropic says it used Claude to prove security properties at the assembly code level (RISC-V) in more than 100 real-world open-source libraries. The team believes this is the first large-scale effort to use AI to apply formal verification to production software at that level. While writing the proofs, Claude also found bugs that had gone undetected for years, despite trillions of test runs.

The urgency is clear from the source: even the Linux kernel, one of the most heavily tested pieces of software and deployed on billions of devices, recently had over 1,000 vulnerabilities disclosed. Formal verification works by translating code into a mathematical model and trying to prove it always follows defined security rules. A failed proof signals a possible bug, and repeating the process after each fix can ultimately show the code has no bug that breaks those rules. Anthropic expects this approach to become essential to secure software development as models improve.