LLMs Make Formal Software Verification Possible at a Much Larger Scale

At a glance

Software bugs can be easily found and exploited by AI, so traditional security defenses alone are not enough. Formal verification, a method that mathematically proves a program has no bugs, is effective but has until now required a great deal of expert time. In this study, Claude produced such proofs for more than 100 open-source libraries.

Key points

1. 1

   Claude proved security properties at the level of assembly code, which is close to machine language, based on the RISC-V instruction set.

2. 2

   While writing the proofs, Claude found bugs that had gone undetected for years despite trillions of tests.

3. 3

   The proofs only hold under certain assumptions, such as single-threaded execution and fixed memory conditions.

4. 4

   The researchers said this approach is still far from fixing every bug, but it shows a path toward that goal.

Why it matters

If it becomes possible to prove that a program always terminates normally without memory errors, it could help prevent security incidents before they happen.