Anthropic poinformował 22 października 2026 r., że Claude i firma Theorem przygotowali dowody braku awarii dla 239 punktów wejścia w 123 bibliotekach z Google OSS-Fuzz. Jądro Rocq sprawdzało te dowody dla wejść mniejszych niż 64 MB, ale w ramach określonego modelu programu i systemu, a nie całych bibliotek w każdej możliwej konfiguracji.
Jak Claude i Rocq współpracowały przy dowodach
Fuzzing to automatyczne testowanie programu z użyciem wielu wygenerowanych danych wejściowych. Anthropic i Theorem wykorzystali istniejące testy fuzz jako podstawę specyfikacji, czyli formalnego opisu sprawdzanej właściwości. Następnie Claude generował kod dowodu dla skompilowanych programów RISC-V, a jądro Rocq sprawdzało, czy dowód wynika ze specyfikacji. Theorem dostarczył semantykę instrukcji RISC-V i procesów Linuksa, czyli formalny opis ich działania używany w tym sprawdzeniu.
Animacja przedstawia drogę od kodu i pliku wykonywalnego RISC-V przez specyfikację do dowodu sprawdzanego przez Rocq. Jest po angielsku i ilustruje opisywany przebieg.
Co dokładnie obejmował wynik
Wynik dotyczył właściwości „brak awarii” dla każdego wejścia krótszego niż 64 MB w wybranym punkcie wejścia. Anthropic opisał model jako jednowątkowy, statyczny program RISC-V z ustalonym budżetem pamięci, działający według modelu Linuksa. Sprawdzone programy miały medianę długości 18 tys. instrukcji RISC-V.
Liczby 239 i 123 oznaczają odpowiednio sprawdzone punkty wejścia i biblioteki, z których je wybrano. Anthropic zaznaczył, że nie zweryfikowano wszystkich punktów wejścia w tych bibliotekach. Dowód dla wybranego punktu nie obejmuje automatycznie każdego sposobu użycia biblioteki ani kodu, do którego ten punkt nie prowadzi.
Błędy ujawnione podczas prób dowodzenia
Anthropic podał, że Claude poprawiał błędy napotkane podczas prób dowodzenia, a następnie generował specyfikację dla poprawionego kodu. W jednym z przykładów przepełnienie licznika w dekompresorze prowadziło do zapisu poza zakresem przy rzadkim układzie danych wejściowych o rozmiarze około 20 MB. W innym odczyt poza zakresem w dekoderze obrazu wymagał wejścia o rozmiarze 64 MB i ponad 2 GB pamięci.
Anthropic opisał też błąd odczytu poza zakresem zależny od określonej sekwencji wywołań dotyczących dwóch uchwytów do tego samego pliku oraz ponowne wykrycie CVE-2026-56132 w bibliotece libexpat. Są to przykłady błędów zgłoszonych w relacji z projektu.
Dlaczego dowód nie jest certyfikatem całej biblioteki
Rocq sprawdza, czy dowód spełnia specyfikację. Samo sprawdzenie nie rozstrzyga, czy specyfikacja opisuje wszystkie zachowania istotne w rzeczywistym wdrożeniu. Wynik zależy więc od właściwości zapisanej w twierdzeniu, modelu maszyny oraz kodu objętego sprawdzeniem.
Anthropic wskazał również, że AddressSanitizer, narzędzie używane przez OSS-Fuzz do wykrywania niektórych błędów pamięci w kodzie C i C++, nie wykrywa ich wszystkich. Sprawdzenie wybranych punktów wejścia nie obejmuje też automatycznie błędów w kodzie wywołującym bibliotekę ani w nieosiąganych fragmentach programu.
Co aneks wyjaśnia o skali dowodów i interpreterze Pythona
Aneks rozróżnia około miliarda linii Rocq wygenerowanych podczas prób od około 180 mln linii w dowodach, które przeszły sprawdzenie. Typowy ukończony dowód miał około 600 tys. linii rozłożonych na mniej więcej 1400 plików, a jego sprawdzanie zajmowało od 30 minut do kilku godzin pracy procesora. Łączna liczba wygenerowanych linii opisuje wszystkie próby, a nie wyłącznie zaakceptowane dowody.
W odrębnym studium przypadku narzędzie Verus sprawdziło wszystkie 17 poziomów interpretera Pythona napisanego w Rust względem formalnej semantyki projektu. Porównanie z CPython miało charakter empiryczny: w ponad 1,7 mln wygenerowanych programów zgodność zachowania wyniosła 99,95%. Ten wynik testów nie jest formalnym dowodem równoważności z CPython dla każdego programu.
