- Published on
LLMs are making formal software verification feasible at a much larger scale
- Authors
- Name
- DeepHorus
In a collaboration with Theorem, researchers used LLMs to formally verify security properties in over 100 real-world open-source libraries at the assembly code level (RISC-V). This marks the first large-scale effort to apply AI-driven formal verification to production software at the assembly level. The team used Claude to produce formal proofs autonomously.
Most software contains bugs, and AI can increasingly exploit them. The Linux kernel recently had over 1,000 vulnerabilities disclosed despite being heavily tested. Formal verification could prove code free of bugs, but it has historically required years of expert effort. For example, verifying the seL4 kernel took 20 person-years.
Claude proved that 123 open-source libraries will always exit normally without memory-safety errors or failed assertions for every input under 64 MB. This holds under assumptions including a single-threaded static binary with a fixed memory budget on a RISC-V CPU using Linux. The proofs also uncovered bugs that had eluded detection for years despite trillions of test runs.
This demonstrates that LLMs can now produce formal proofs at large scale, enabling new workflows with proven security guarantees. While it does not yet eliminate all bugs, it provides a roadmap toward that goal. The approach gets much closer to comprehensive bug-free code than before.
The team is publishing a subset of the proofs for anyone to verify and reuse, along with the RISC-V and OS semantics. Theorem is offering to run the same pipeline for other projects. This openness aims to accelerate adoption of formal verification.
As model capabilities continue to improve, the researchers expect formal verification to become an essential part of secure software development. They envision a future where proven security guarantees are standard. The researchers believe this shift will fundamentally change how software is built and secured.
