LLMs Are Now Proving Software Correct — Anthropic's Formal Verification at Scale
By Arash Latifi
Anthropic used Claude to prove security properties of 123 real open-source libraries at the RISC-V assembly level. Formal verification goes from 20 person-years to automated.
TL;DR — Anthropic proved security properties of 123 real open-source libraries at the RISC-V assembly level using Claude; work that once took 20 person-years is becoming automated.
Why nobody did this before
Most software is full of bugs, and testing only exercises some inputs. Formal verification flips this: you translate code into a mathematical model and prove it always satisfies defined security rules — for every input. When a proof fails, the failure itself points at the bug.
The problem is cost. Proofs are often far longer than the code itself. Anthropic's own example: implementing the seL4 kernel took 2 person-years; formally verifying it took 20. That's why formal verification was confined to truly mission-critical code like Airbus avionics.
What Anthropic did
Working with Theorem, they used Claude to prove security properties across 123 real open-source libraries:
- Proofs are at the RISC-V assembly level — per their own claim, the first large-scale AI effort to formally verify production software at that level.
- The proven property: programs always exit normally without memory-safety errors or failing assertions, for every input under 64 MB and every modeled Linux response — assuming a single-threaded static binary with a fixed memory budget on RISC-V.
- While writing proofs, Claude found bugs that had eluded detection despite trillions of test runs.
- A subset of the proofs is published so anyone can verify them independently.
The paper also notes the Linux kernel — among the most tested software on Earth — recently had over 1,000 vulnerabilities disclosed. Testing alone clearly isn't enough.
| Method | What it guarantees | Traditional cost | With LLMs | | --- | --- | --- | --- | | Testing (unit/E2E) | Only tested inputs | Low | unchanged | | Fuzzing | Random inputs | Medium | unchanged | | Formal verification | All inputs, mathematically | ~10× code size (20 person-years for seL4) | automated at scale |
What it means for everyday developers
You won't be writing Lean for your storefront tomorrow. But three practical consequences are near:
- Proofs in CI. If a model can generate proofs, a PR pipeline can regenerate and check them. Future reviews may read "tests pass, security proof passes."
- Auditable dependencies. If the libraries you install carry memory-safety proofs, supply-chain risk genuinely drops instead of just being claimed.
- The engineer's role shifts. Proof-writing becomes model output + human review, much like code review. Your value moves to defining the right security properties.
Readiness checklist
- [ ] Identify your critical modules (auth, payments, crypto)
- [ ] Get line coverage on those modules to 100% first
- [ ] Enable strict static analysis (type checkers, linters) in CI
- [ ] Pin dependency versions and lockfiles so audits are possible
- [ ] Read the Anthropic paper and published proofs to learn what acceptable output looks like
FAQ
Q: Does this mean no more security bugs?
No. The proofs hold under assumptions (single-threaded, fixed memory budget, RISC-V). Outside those assumptions nothing is guaranteed. Formal verification adds a stronger layer, not absolute safety.
Q: Should I learn Lean or Coq?
If you work on critical systems, yes — the concepts matter. But the paper's core message is that LLMs now carry the proof-writing burden; your value is in specifying properties precisely and reviewing proofs.
Q: Is this useful for my Next.js/web project today?
Not directly — the proofs were at the assembly level for system libraries. The near-term takeaway for web devs: push stronger static analysis now, and expect AI tooling to produce verifiable output rather than just code.