The lede
LLMs are making formal software verification feasible at a much larger scale
Anthropic · made the Sunday
Formal verification has always been the technique everyone admires and nobody uses — seL4 took two person-years to build and twenty to prove — and the move here is a shortcut past the hardest part of it: instead of writing a specification by hand, Anthropic and Theorem convert a project's existing fuzz tests into one, encoding the rule "this suite always passes" over a full model of a RISC-V binary running on Linux, and then let Claude grind out the proof. It held for 123 open-source libraries, proving they exit normally with no memory-safety error or failed assertion for every input under 64MB and every modeled OS response, and along the way it surfaced bugs that trillions of fuzz runs had never hit. The proofs and the RISC-V/OS semantics are published, Theorem will run the pipeline on your repo, and there is a skill for doing it yourself — which makes this the rare research post with a next step attached.