Anthropic says Claude proved security properties in 123 open-source libraries at the RISC-V assembly level
- Anthropic used Claude to prove security properties at the RISC-V assembly level across 123 open-source libraries, which Anthropic calls the first large-scale effort of its kind on production software.
- The proofs show that the programs always exit normally without memory-safety errors or failed assertions for every input under 64 MB, assuming a single-threaded static binary with a fixed memory budget on Linux.
- While writing the proofs, Claude found bugs that had escaped detection for years despite trillions of test runs.
- SeL4 took 2 person-years to implement and 20 person-years to formally verify, which is why formal verification has mostly been limited to mission-critical code like Airbus avionics.
- Theorem, the collaborator on the project, is offering to run the same pipeline for other open-source projects and published a Claude skill to help developers verify their own code.
Hacker News 의견들
Agent proofs being this verbose is the scary part. Some earlier project hit a complexity wall and needed modular abstractions to scale, so the real question is whether agents can learn those abstractions.
Writing proofs is just writing code in a niche language, Curry-Howard and all. If you train agents to write modular proofs, they probably get better at programming in general, and maybe at Haskell and Rust too.
People call LLM math output creative because the training corpus is huge. But they interpolate well and extrapolate badly. Give one a real insight and it writes a proof for it, but it won't come up with the novel idea by itself.
Sounds like a software problem.
The difference is that in math the bottleneck is out-of-distribution generalization, so the convex hull limit bites. In software verification the bottleneck is mostly scale, so you can verify a huge amount of existing code even if the hull limit is real.
I love the convex hull analogy. I think LLMs are more useful as a way to spread knowledge to people who lacked money, time, or expertise than as actual intelligence.
I agree with the observation but not the conclusion. RL on sufficiently hard problems might push agents toward better proof strategies on their own.
The appendix says agent proofs keep spelling out register contents, integer conversions, and every branch. Human proof engineers would have factored all that out immediately.
This matches what I see. LLM-written tests hard-code everything, so any harmless change to the source breaks them and they catch nothing that matters.
Strange to see Anthropic making this point. Claude doesn't do formal verification unless I tell it to, even when it could quickly write scripts to check the system state it's assuming.
Unit tests are worthless when humans write them and worse when AI writes them, since you're just testing yourself and of course you pass.
If you want it to do that every time, why not put it in your CLAUDE.md?
How do you know your model matches the program? You could prove something that isn't your actual program.
If you model the language, you prove things about the source. Model the ISA too and you can prove things about the binary, which sidesteps compiler bugs. Then you only assume your hardware matches the model.
Correct, it can happen. The real code can diverge from the Lean model in a glaring or subtle way.