Anthropic twierdzi, że Claude napisał formalne dowody na to, że 123 biblioteki open source nie ulegają awarii

We współpracy z Theorem Anthropic twierdzi, że wykorzystało Claude do udowodnienia właściwości bezpieczeństwa na poziomie asemblera (RISC-V) w ponad 100 rzeczywistych bibliotekach open source. Firma określa to jako pierwsze zastosowanie AI na dużą skalę do formalnej weryfikacji oprogramowania produkcyjnego na tym poziomie.

Według Anthropic:

• Co udowodniono: dla 239 punktów wejścia testów fuzzingowych w 123 bibliotekach OSS-Fuzz programy zawsze kończą działanie prawidłowo, bez błędów bezpieczeństwa pamięci i nieudanych asercji, dla każdego wejścia o rozmiarze poniżej 64 MB. Obowiązuje to przy założeniu, że chodzi o statyczny plik binarny działający jednowątkowo, ze stałym limitem pamięci, na procesorze RISC-V z systemem Linux. Dowody liczą łącznie około 180 milionów wierszy kodu Rocq, sprawdzonych przez weryfikator dowodów Rocq.
• Jak: istniejący test fuzzingowy każdej biblioteki przekształcono w specyfikację („ten test nigdy nie powoduje awarii”), a Claude napisał dowód, po drodze poprawiając wykryte błędy. Anthropic twierdzi, że w ten sposób znaleziono setki błędów, w tym takie, do których fuzzer raczej by nie dotarł, jak zapis poza zakresem wymagający rzadkiego wejścia o rozmiarze 20 MB, a także ponownie odkryto CVE-2026-56132 w libexpat.
• Inne eksperymenty: Claude udowodnił, że implementacja zlib w jądrze Linux odpowiada specyfikacji RFC 1950 na poziomie pliku binarnego x86, a także stworzył interpreter Pythona w Rust, którego działanie zgadzało się z CPython w 99,95% z 1,7 miliona losowych programów. Anthropic twierdzi również, że próby formalnej weryfikacji popularnego czytnika PDF ujawniły w ciągu tygodnia tyle samo błędów bezpieczeństwa, ile zwykle zgłasza się w ciągu roku.
• Koszt: dowody mogą wymagać setek milionów tokenów. Anthropic twierdzi, że w 36 niewielkich zadaniach weryfikacyjnych Opus 5.5 udowadnia połowę z nich, zużywając około 40% mniej tokenów niż Opus 5, a agenci współdzielący dowody potrzebowali o 17% mniej tokenów.

Anthropic publikuje część dowodów oraz semantykę RISC-V i Linux. Theorem oferuje uruchomienie tego samego procesu dla innych projektów open source i publikuje umiejętność Claude do weryfikowania własnego kodu. Anthropic zaznacza, że nie dowodzi to, iż biblioteki są wolne od błędów: pozostałe błędy znajdowałyby się w zaufanych komponentach lub poza zakresem dowodów.