Anthropic and Theorem used Claude to patch and verify 239 fuzzing entry points across 123 open-source libraries, proving that they do not crash for inputs smaller than 64 MB. A proof checker validates roughly 180 million lines of Rocq code. The guarantees assume single-threaded, statically linked RISC-V binaries with fixed memory budgets and a Linux execution model; they do not establish that entire libraries are bug-free. The separate Vero evaluation likewise distinguishes passing individual specifications from completing every proof in a repository, underscoring the importance of checking proof scope and trusted foundations.