Anthropic twierdzi, że Claude udowodnił właściwości bezpieczeństwa w 123 bibliotekach

22 października 2026 r. Anthropic opublikowało badania, w których poinformowało, że we współpracy z Theorem Claude opracował sprawdzone maszynowo formalne dowody właściwości bezpieczeństwa na poziomie kodu asemblera RISC-V dla 239 punktów wejścia testów fuzzingowych w 123 bibliotekach open source.

Według Anthropic Claude naprawił znalezione błędy, a następnie udowodnił, że programy zawsze kończą działanie normalnie, nie powodując błędów bezpieczeństwa pamięci ani niepowodzeń asercji — dla każdego wejścia o rozmiarze poniżej 64 MB oraz każdej modelowanej reakcji systemu operacyjnego Linux i każdego układu pamięci. Dowody zakładają, że program działa jako jednowątkowy plik binarny o stałym budżecie pamięci na procesorze RISC-V z systemem Linux. Anthropic poinformowało, że dowody obejmują około 180 milionów wierszy kodu Rocq, a typowy dowód liczy około 600 000 wierszy i dotyczy plików binarnych o medianowej długości 18 000 instrukcji RISC-V. Firma stwierdziła, że według jej wiedzy jest to pierwsza zakrojona na dużą skalę próba wykorzystania AI do formalnej weryfikacji oprogramowania produkcyjnego na poziomie kodu asemblera.

Część dowodów, a także leżące u ich podstaw semantyka RISC-V i systemu operacyjnego, jest publikowana w serwisie GitHub. Anthropic poinformowało również o udostępnieniu zbudowanych na potrzeby projektu zaufanych komponentów, które nie były wcześniej publicznie dostępne, kompletnych dowodów dla testów fuzzingowych niewymagających poprawek oraz specyfikacji testów, których nie udało się udowodnić. Firma nie udostępnia natomiast dowodów, które mogłyby ujawnić nienaprawiony błąd.

Przekształcanie testów fuzzingowych w formalne dowody

W ramach tego podejścia istniejący, kompilowalny test fuzzingowy każdej biblioteki jest przekształcany w formalną specyfikację kodującą jedną regułę: test nigdy nie ulega awarii dla żadnego wejścia o rozmiarze poniżej 64 MB. Specyfikację definiuje się na podstawie skompilowanych instrukcji RISC-V, wykorzystując formalną semantykę zestawu instrukcji RISC-V i procesów Linuksa opracowaną przez Theorem, a weryfikator dowodów Rocq sprawdza każdy ukończony dowód pod kątem zgodności ze specyfikacją. Anthropic twierdzi, że dzięki temu programiści muszą ufać tylko trzem komponentom: formalnym modelom RISC-V i procesów Linuksa, dokładnym sformułowaniom twierdzeń oraz samemu weryfikatorowi Rocq.

Anthropic poinformowało, że zastosowało tę metodę do setek projektów w ramach inicjatywy OSS-Fuzz firmy Google, która zapewnia ciągłe testy fuzzingowe kwalifikującym się projektom open source oraz automatycznie instrumentuje programy w C i C++ za pomocą AddressSanitizer — narzędzia, które powoduje awarię programu za każdym razem, gdy pamięć jest używana w nieprawidłowy sposób. W załączniku datowanym na 22 października 2026 r. przedstawiono pełne udowodnione twierdzenie: dla wszystkich wejść o rozmiarze poniżej 64 MiB i wszystkich układów pamięci ani plik binarny instrumentowany za pomocą ASan, ani zwykły plik binarny nie ulega awarii, nie przerywa działania ani nie wykazuje niemodelowanego zachowania, a oba generują identyczne ślady odczytu i zapisu, zachowanie przy kończeniu działania oraz końcowy stan systemu plików.

W załączniku podano, że podczas prac Claude napisał około miliarda wierszy kodu Rocq, z czego około 180 milionów przeszło kontrolę weryfikatora dowodów. Dowód dotyczący 391-wierszowego punktu wejścia parsera cJSON liczył 630 000 wierszy, a dowód dla fftw3, z którą połączono 51 000 wierszy kodu, miał 480 000 wierszy. Ponieważ Claude mógł poprawiać kod przed ukończeniem dowodu, Anthropic poinformowało, że wprowadziło kary za poprawki, przyznawało dodatkowe punkty za udowodnienie, które wejścia zmieniła dana poprawka, a także rejestrowało i audytowało poprawki, aby zniechęcić do wykorzystywania mechanizmu nagród.

Błędy wykryte podczas prób przeprowadzenia dowodów

Anthropic informuje, że próby przeprowadzenia dowodów ujawniły setki błędów, z których wielu fuzz tester prawdopodobnie by nie wykrył. Podczas dowodzenia poprawności punktu wejścia jednej z bibliotek Claude znalazł niedomiar licznika w dekompresorze, który powodował zapis poza zakresem, ale tylko dla wejść o wielkości około 20 MB i jednym rzadkim, konkretnym układzie. Wśród pozostałych znalezisk znalazł się odczyt poza zakresem w dekoderze obrazów, wymagający wejścia o wielkości 64 MB i ponad 2 GB pamięci; odczyt poza zakresem wymagający określonej sekwencji wywołań z użyciem dwóch uchwytów do tego samego pliku; oraz ponowne odkrycie luki CVE-2026-56132 w libexpat, której wykorzystanie wymagało głęboko zagnieżdżonego wejścia.

Claude znalazł również błędy logiczne, które nigdy nie powodują awarii, w tym przypadek, w którym ograniczenie określające, jakie pliki może wczytywać aplikacja, nie zawsze jest egzekwowane. Anthropic poinformowało, że próby weryfikacji kilku szeroko wykorzystywanych aplikacji o krytycznym znaczeniu ujawniły wcześniej nieznany błąd logiczny, który pozostawał ukryty przez ponad dekadę. Firma dodała też, że podczas próby weryfikacji szeroko używanego czytnika PDF znalazła w ciągu tygodnia tyle błędów bezpieczeństwa, ile zazwyczaj zgłasza się w ciągu roku.

Dodatkowe eksperymenty i wnioski dotyczące wydajności

Poza OSS-Fuzz Anthropic poprosiło Claude’a o napisanie formalnej specyfikacji RFC 1950, dokumentu technicznego definiującego format kompresji zlib, a następnie o udowodnienie, że implementacja zlib w jądrze Linuksa prawidłowo ją realizuje. Claude bezpośrednio udowodnił poprawność pliku binarnego skompilowanego dla x86, korzystając z wygenerowanej przez siebie formalnej semantyki zestawu instrukcji x86. Anthropic poinformowało, że powtórzyło ten proces dla pół tuzina innych szeroko używanych bibliotek, wykrywając drobne, niemożliwe do wykorzystania błędy w przypadkach brzegowych, które są zgłaszane zespołom utrzymującym te projekty. Firma podała również, że podczas generowania semantyki x86 wykryto setki błędów w oficjalnej dokumentacji referencyjnej oraz mniejszą liczbę błędów w samym sprzęcie, a krokowe wykonywanie semantyki może uruchomić środowisko użytkownika Ubuntu na jądrze Linuksa.

W innym eksperymencie Claude stworzył w języku Rust interpreter obsługujący dużą część Pythona i udowodnił za pomocą narzędzia weryfikacyjnego Verus, że działa on zgodnie z semantyką CPython opisaną w artykule naukowym. Dodatek techniczny podaje, że udowodniono poprawność wszystkich 17 poziomów interpretera, a twierdzenie brzmi: „Za każdym razem, gdy interpreter zwraca wynik, jest to wynik przewidziany przez semantykę formalną”. Anthropic poinformowało, że w testach empirycznych przeprowadzonych na 1,7 mln losowo wygenerowanych programów w Pythonie zachowanie interpretera było identyczne z CPython w 99,95% przypadków; spośród siedmiu celowo wprowadzonych błędów pięć przetrwało testy losowe, a wszystkie siedem powodowało niepowodzenie dowodu.

Aby zmierzyć wydajność, Anthropic stworzyło 36 niewielkich zadań weryfikacyjnych, zmniejszając rzeczywiste punkty wejścia OSS-Fuzz. Powstały programy zawierające od 283 do 2 491 instrukcji, z danymi wejściowymi ograniczonymi do 64 bajtów; AddressSanitizer zastąpiono środowiskiem uruchomieniowym „mini-ASan”, liczącym około 100 instrukcji. Anthropic podaje, że Opus 5.5 rozwiązuje połowę zadań, używając o około 40% mniej tokenów niż Opus 5. Anthropic informuje również, że agenci, którym umożliwiono kopiowanie dowodów od siebie nawzajem we wspólnej przestrzeni roboczej, potrzebowali o 17% mniej tokenów niż agenci pracujący samodzielnie; niektórym udało się rozwiązać zadania po wcześniejszym niepowodzeniu w pracy indywidualnej, a agenci pracujący samodzielnie nie ukończyli dwóch dowodów. Firma podała, że podobny efekt ponownego wykorzystania rozwiązań wystąpił na większą skalę podczas prac nad OSS-Fuzz: zespoły agentów kopiowały ukończone dowody i dostosowywały je, ponieważ znaczna część każdego dowodu dotyczy wspólnego kodu środowiska uruchomieniowego C oraz kodu inicjalizującego AddressSanitizer.

Deklarowane ograniczenia i program OSS Verify

Anthropic zaznacza, że dowody nie oznaczają, iż biblioteki są wolne od błędów: pozostałe błędy mogą znajdować się w zaufanych komponentach albo poza zakresem dowodów. Dowody dotyczą jednowątkowych, statycznych plików binarnych dla architektury RISC-V, połączonych z musl libc, podczas gdy większość użytkowników korzysta z tych bibliotek na platformach x86 lub ARM i łączy je dynamicznie z glibc; ponadto AddressSanitizer nie wykrywa wszystkich błędów związanych z bezpieczeństwem pamięci. Firma poinformowała, że spodziewa się, iż wraz z rozwojem modeli ograniczenia te staną się możliwe do przezwyciężenia.

Theorem udostępnia bezpłatnie ten sam proces kwalifikującym się projektom open source w ramach programu OSS Verify. Zgłoszenie projektu odbywa się przez pull request dodający do repozytorium programu pliki project.yaml, Dockerfile i build.sh. Theorem informuje, że ocenia projekty według kryteriów podobnych do stosowanych w OSS-Fuzz, nadając priorytet szeroko wykorzystywanej infrastrukturze krytycznej. Według Theorem opiekunowie projektów otrzymują dowód w systemie Rocq, sprawdzony przez jądro Rocq, potwierdzający, że żaden cel fuzzingu nie ulega awarii dla żadnego wejścia o rozmiarze do 64 MiB; błędy wykryte podczas pracy nad dowodem są zgłaszane opiekunom prywatnie, pocztą elektroniczną, bez wyznaczonego terminu ich ujawnienia, a przygotowanie dowodów może zająć kilka dni. Plan rozwoju Theorem zakłada weryfikację całego ekosystemu Nix, w tym infrastruktury krytycznej, takiej jak glibc, OpenSSL i cURL.