Claude udowodnił bezpieczeństwo kodu 123 bibliotek open source. 180 milionów linii dowodów w kilka tygodni

Formalna weryfikacja, czyli matematyczny dowód, że program nie zawiedzie w zdefiniowanych warunkach, od dekad była luksusem. Zespół specjalistów potrzebował 20 osobolat, żeby zweryfikować niewielkie jądro systemu operacyjnego seL4. Dlatego metodę stosowano głównie tam, gdzie błąd kosztuje najwięcej, na przykład w oprogramowaniu awionicznym Airbusa. Anthropic twierdzi, że to się zmienia: zespół Frontier Red Team wraz z partnerem Theorem oddał pracę nad dowodami Claude’owi. Opisuje to w materiale na swojej stronie, a streszcza The Decoder.

Skala: 239 punktów wejścia, 123 biblioteki

Projekt objął 239 punktów wejścia w 123 bibliotekach z Google OSS-Fuzz, czyli inicjatywy do automatycznego fuzzingu projektów open source. Claude nie pisał nowego kodu. Zamieniał istniejące testy w problemy matematyczne, analizował skompilowany kod maszynowy (binaria RISC-V) i budował do nich dowody. Według Anthropic powstało około 180 mln linii dowodów w języku Rocq, a prób, które do tego doprowadziły, było około miliarda linii. Typowy dowód liczył około 600 tys. linii, a mediana weryfikowanego binarium to 18 tys. instrukcji RISC-V.

Poprawność dowodów sprawdza niezależny program, jądro Rocq. Dzięki temu proces wymaga według Anthropic niemal zerowego udziału ludzi-recenzentów. Autorzy nazywają generowanie dowodów „w pełni autonomicznym”, choć sami przyznają, że narzędzia i formalne podstawy zbudowali ludzie z Theorem.

Błędy znalezione po drodze

Claude natrafił na setki błędów i mógł je sam naprawiać. Część ujawnia się tylko w rzadkich warunkach, takich jak nietypowo duży plik wejściowy czy szczególna sekwencja odwołań do pamięci. Przez takie dziury zwykłe testy, także fuzzingowe, potrafią przejść bez zarzutu. Przy weryfikacji popularnego czytnika PDF zespół znalazł w tydzień tyle błędów bezpieczeństwa, ile zwykle zgłasza się dla tego programu przez cały rok. W innym przypadku model wykrył błąd logiczny, który przez ponad dekadę pozostawał niezauważony. Anthropic zaznacza, że nawet gdy pełny dowód się nie udaje, sama próba często wydobywa realne błędy.

Efekt końcowy to według firmy dowód, że po poprawkach naniesionych przez Claude’a nie da się wywołać awarii żadnym wejściem do 64 MB we wszystkich 239 punktach wejścia. Dowody dla części przypadków są dostępne w repozytorium Theorem.

Ograniczenia

„Formalnie zweryfikowany” nie znaczy „wolny od błędów”, i Anthropic sam to podkreśla. Dowody obowiązują tylko w wąskich warunkach: dla konkretnej architektury (RISC-V/Linux), programów jednowątkowych i danych wejściowych poniżej 64 MB. W praktyce biblioteki działają na różnym sprzęcie i w różnych konfiguracjach.

Drugim ograniczeniem jest koszt obliczeń. Pojedyncze dowody pochłaniały setki milionów tokenów, a firma nie podaje łącznego kosztu projektu. Według The Decoder nowsze modele radzą sobie taniej: Opus 5.5 rozwiązuje połowę dowodów, zużywając około 40 proc. mniej tokenów niż Opus 5. Mniejszy test pokazał też, że dowody da się ponownie wykorzystywać.

Anthropic oczekuje, że formalna weryfikacja wspierana przez AI stanie się wkrótce równie rutynowa jak zwykłe testowanie. Plany Theorem sięgają już po infrastrukturę krytyczną: glibc, OpenSSL i cURL. Jeśli to się sprawdzi, pytanie o programowanie z pomocą AI przesunie się z „czy model potrafi napisać kod” na „czy potrafi udowodnić, że ten kod jest bezpieczny”. Pozostaje pamiętać, że odpowiedź zawsze będzie dotyczyć tylko tych warunków, które ktoś wcześniej zdefiniował.