Anthropic używa Claude do formalnej weryfikacji kodu 123 bibliotek open source

22 października 2026 roku Frontier Red Team Anthropic opisał projekt prowadzony z firmą Theorem, w którym Claude pisał formalne dowody dla prawdziwego oprogramowania open source. Claude zamienił istniejące testy fuzzingowe z OSS-Fuzz w specyfikacje i udowodnił, że 239 punktów wejścia w 123 bibliotekach nie ulega awarii dla żadnych danych mniejszych niż 64 MB. Dowody dotyczą skompilowanych plików binarnych RISC-V, liczą łącznie około 180 milionów linii w Rocq i sprawdza je program Rocq, więc nie trzeba ich przeglądać ręcznie.

Podczas pisania dowodów Claude znalazł i poprawił błędy, których fuzzing nie wykrył. Jednym z nich był zapis poza zakresem bufora w dekompresorze, który pojawiał się tylko przy danych o rozmiarze około 20 MB. Claude ponownie odkrył też lukę CVE-2026-56132 w libexpat. Inne eksperymenty objęły kod zlib w jądrze Linuksa i interpreter Pythona napisany w Rust.

Anthropic wymienia ograniczenia. Dowody zakładają jednowątkowy, statycznie zlinkowany program na Linuksie z RISC-V i musl, a większość użytkowników korzysta z x86 lub ARM z glibc. AddressSanitizer nie wykrywa też wszystkich błędów pamięci. Dowody mogą wymagać setek milionów tokenów. W 36 zadaniach testowych Opus 5.5 udowodnił połowę z nich, zużywając o około 40% mniej tokenów niż Opus 5. Część dowodów oraz semantyka RISC-V i systemu operacyjnego są publicznie dostępne, a Theorem oferuje uruchomienie tego samego procesu dla innych projektów open source.