# Anthropic uses Claude to prove security properties in 123 open-source libraries

> Original title: LLMs are making formal software verification feasible at a much larger scale

- Source: Hacker News · AI (150+ points)
- Published: 2026-10-22T22:54:43.000Z
- Bad Influence: https://badinfluence.news/items/u92qxu4djzj1cwexfb6zxufyb
- Original: https://www.anthropic.com/research/formal-verification

## Summary

Anthropic says Claude proved no-crash properties across 239 OSS-Fuzz entry points in 123 open-source libraries, working on compiled RISC-V binaries. The proofs were checked by the Rocq proof checker, and Claude also found and fixed bugs during the process. The post notes that formal verification does not mean bug-free, since the trusted RISC-V, Linux, and Rocq components remain assumptions.