Claude i Theorem. Formalne dowody bezpieczeństwa dla 123 bibliotek open source

Czym jest formalna weryfikacja kodu

Testy i fuzzing, czyli zasypywanie programu losowymi danymi, pokazują, że kod działa dla sprawdzonych przypadków. Formalna weryfikacja idzie dalej. Matematyczny dowód wykazuje, że dana własność zachodzi dla wszystkich możliwych danych wejściowych, także tych, których nikt nie przetestował.

Do tej pory metoda była opłacalna głównie dla małych fragmentów kodu, bo pisanie dowodów wymagało tygodni pracy ekspertów. Anthropic twierdzi, że modele językowe zmieniają ten rachunek. Zaletą podejścia jest to, że nie trzeba ufać samemu modelowi. Każdy dowód sprawdza niezależny program Rocq, a nie człowiek ani Claude.

Co dokładnie udowodnił Claude

Punktem wyjścia były testy z OSS-Fuzz, programu Google, który od lat stale testuje najważniejsze projekty open source. Każdy test Claude zamienił w specyfikację mówiącą, że program nigdy nie ulega awarii dla wejścia mniejszego niż 64 MB. Następnie napisał dowód, że skompilowany plik binarny zawsze kończy działanie normalnie, bez naruszenia pamięci i bez nieudanej asercji.

Dowody działają na poziomie instrukcji procesora RISC-V, a nie kodu źródłowego. Dzięki temu obejmują także błędy wprowadzone przez kompilator. Typowy dowód ma ok. 600 tys. linii i dotyczy programu z medianą 18 tys. instrukcji. Cały projekt zajął kilka tygodni, a formalny model procesora RISC-V i procesu w Linuksie dostarczyła firma Theorem.

Jakie błędy wykryto przy okazji

Dowodu nie da się napisać dla kodu, który zawiera błąd. Dlatego próby weryfikacji ujawniły setki usterek. Claude je łatał, a specyfikacje generowano od nowa na podstawie poprawionego kodu. Anthropic opisuje m.in. takie przypadki:

• przepełnienie licznika w dekompresorze prowadzące do zapisu poza buforem, ujawniające się dopiero przy wejściu ok. 20 MB i rzadkim układzie pamięci,
• odczyt poza buforem w dekoderze obrazów, wymagający wejścia 64 MB i ponad 2 GB pamięci,
• odczyt poza buforem przy określonej sekwencji wywołań na dwóch uchwytach do tego samego pliku,
• ponowne odkrycie luki CVE-2026-56132 w bibliotece libexpat do przetwarzania XML,
• błąd logiczny, przez który ograniczenie wczytywania plików nie zawsze działało.

Inne eksperymenty i koszt w tokenach

W osobnym eksperymencie Claude napisał specyfikację formatu zlib według RFC 1950 i udowodnił, że implementacja z jądra Linuksa jest z nią zgodna na poziomie kodu x86. Powtórzono to dla ok. sześciu innych bibliotek. Model zbudował też interpreter podzbioru Pythona w języku Rust i za pomocą narzędzia Verus udowodnił jego zgodność z CPythonem. Na 1,7 mln losowych programów zachowanie było identyczne w 99,95 proc. przypadków.

Anthropic nie podał kosztu projektu w dolarach. Pojedynczy dowód może wymagać setek milionów tokenów. W teście na 36 mniejszych zadaniach Claude Opus 5.5 zużywał ok. 40 proc. mniej tokenów niż Opus 5, aby udowodnić połowę zadań. Agenci pracujący we wspólnej przestrzeni roboczej zużywali o 17 proc. mniej tokenów niż agenci działający osobno.

Granice metody

Sam Anthropic zastrzega, że formalnie zweryfikowany kod nie jest automatycznie wolny od błędów. Dowód gwarantuje tylko to, co zapisano w specyfikacji. Jeśli model procesora lub systemu operacyjnego różni się od rzeczywistości, błąd może się ukryć właśnie w tej różnicy. Zweryfikowano też tylko wybrane punkty wejścia, a nie całe biblioteki.

Najważniejsze ograniczenie dotyczy środowiska. Dowody obejmują jednowątkowe, statycznie linkowane programy na RISC-V z biblioteką musl, podczas gdy większość systemów działa na x86 lub ARM z dynamicznie linkowanym glibc. Aplikacja, która źle wywołuje bibliotekę, nadal może uszkodzić pamięć. Autorzy opisują też ryzyko obchodzenia zadania przez model, który mógłby zmienić program tak, by dowód stał się trywialny. Poprawki Claude były dlatego karane w ocenie i dodatkowo audytowane.

Co to oznacza dla zespołów IT w Polsce

Wynik pojawia się w tygodniu, w którym krytyczne luki PHP2Shell, wykryte z pomocą modeli AI, wymusiły pilne aktualizacje serwerów. Modele coraz szybciej znajdują błędy, więc obrońcy potrzebują metod, które dają silniejsze gwarancje niż testy. Formalna weryfikacja pozostaje na razie narzędziem dla opiekunów najczęściej używanych bibliotek i firm z najwyższymi wymaganiami bezpieczeństwa, a nie dla typowego zespołu aplikacyjnego.

W naszej ocenie polskie zespoły powinny teraz pilnować aktualizacji bibliotek, w których producenci łatają błędy znalezione przez AI, w tym libexpat i zlib. Opiekunowie projektów open source mogą zgłosić projekt do Theorem, który oferuje uruchomienie tego samego procesu, albo przetestować udostępniony skill dla Claude na wybranym module. Dowody, które mogłyby ujawnić niezałatane luki, nie zostały opublikowane.