Anthropic + Theorem: Claude formally verifies 123 OSS libraries at RISC-V assembly level (~180M Rocq lines); first large-scale AI assembly verification claim

Why it matters

【Key points】

Anthropic Frontier Red Team (Oct 22; @AnthropicAI 22:01 UTC) with Theorem: Claude formally verified RISC-V assembly security properties across 123 real OSS libraries—claimed first large-scale AI assembly-level verification of production software.

1. Method: rewrite OSS-Fuzz harnesses as “never crashes for any input <64MB,” prove over RISC-V binaries + Theorem RISC-V/Linux semantics in Rocq. ~239 entry points; ~180M Rocq lines (typical ~600k / ~18k-instruction median binary). Claude also patched bugs found while proving (~20MB underflow, 64MB OOB read, CVE-2026-56132 in libexpat).

2. Also: RFC 1950 + Linux zlib on x86; Verus Rust Python-subset interpreter vs academic CPython; PDF-reader work that surfaced ~a year of security bugs in a week.

3. Release: trusted components + Rocq for unpatched-fuzz proofs; Theorem launches OSS Verify + Claude skill (free for open source).

【Verifiable】

https://www.anthropic.com/research/formal-verification

https://x.com/AnthropicAI/status/2113390212911083894

https://x.com/theoremlabs/status/2113396868814360821

Limits: single-threaded static musl, RISC-V, fixed memory budget.

【Our read】

1. Formal verification has long been priced out (seL4: ~2 person-years to build, ~20 to verify). As models get better at finding exploits, Anthropic pairs “AI offense” with “AI proofs”—a Red Team extension and counterpart to METR/Redwood gaps in OpenAI agent monitoring (e/1039).

2. Vs DeepMind Lean math proofs (e/796) and doubleAI Maxwell rewrite+prove (e/974), this hits OSS-Fuzz and assembly at unusual scale. Caveat: trusted base still includes Rocq, ISA/OS models, and theorem statements—“formally verified” ≠ bug-free.

3. If token cost falls and proofs reuse (~17% fewer tokens shared), verifying shared deps once (glibc/OpenSSL/cURL) becomes credible; spend may tilt from fuzz farms toward proof pipelines.

4. Limits: RISC-V/static/<64MB vs x86/ARM+glibc; specs can diverge from reality; huge token budgets—await independent replay.