Weryfikacja formalna z Claude: dowody dla 123 bibliotek open source

22 października zespół Frontier Red Team z Anthropic razem z firmą Theorem opublikował badanie, w którym Claude napisał formalne dowody bezpieczeństwa dla 123 bibliotek open source z projektu OSS-Fuzz. Dowody dotyczą skompilowanego kodu RISC-V, a nie kodu źródłowego. Według autorów to pierwsza tak duża weryfikacja formalna oprogramowania produkcyjnego na poziomie asemblera z użyciem AI.

Na czym polega weryfikacja formalna z Claude?

Weryfikacja formalna to matematyczny dowód, że program ma określoną własność dla każdego możliwego wejścia, a nie tylko dla tych, które ktoś przetestował. Problem w tym, że dotąd wymagała lat pracy ekspertów. Dla porównania z badania: weryfikacja jądra seL4 zajęła około 20 osobolat, a jego napisanie dwa.

Pipeline z badania wygląda tak:

1. Punktem wyjścia są istniejące testy fuzzingowe z OSS-Fuzz (projektu Google, który bez przerwy zasypuje biblioteki losowymi danymi).
2. Biblioteka razem z testem jest kompilowana do pliku wykonywalnego RISC-V.
3. Z semantyki procesora RISC-V i procesu Linuksa od Theorem automatycznie powstaje specyfikacja: program ma się zawsze zakończyć normalnie, bez błędów pamięci i nieudanych asercji.
4. Claude pisze dowód, a sprawdzarka Rocq potwierdza, że dowód spełnia specyfikację.
5. Gdy Claude trafi na błąd, łata kod, specyfikacja jest generowana na nowo i dowód powstaje od początku.

Gwarancja obejmuje każde wejście poniżej 64 MB i każdą zamodelowaną odpowiedź systemu oraz układ pamięci (przy założeniu statycznego, jednowątkowego programu na RISC-V i Linuksie).

Jakie liczby podał Anthropic?

1. 239 punktów wejścia w 123 bibliotekach.
2. Łącznie około 180 mln linii dowodów w Rocq; typowy dowód ma około 600 tys. linii i dotyczy programu z medianą 18 tys. instrukcji RISC-V.
3. Całość zajęła kilka tygodni.
4. Na 36 małych zadaniach Opus 5.5 udowodnił połowę, zużywając około 40% mniej tokenów niż Opus 5, a agenci pracujący we wspólnej przestrzeni zużyli 17% mniej niż w pojedynkę.

Co ciekawe, dowód dla cpp-httplib wymagał wykazania, że drzewo czerwono-czarne w libc++ ma głębokość ograniczoną logarytmicznie, bo tylko tak dało się wykluczyć przepełnienie stosu w destruktorze std::set.

Jakie błędy znalazł Claude?

Według autorów proces wykrył setki błędów, które przetrwały lata fuzzingu. Przykłady z wpisu:

1. Niedomiar licznika w dekompresorze, który prowadził do zapisu poza buforem, ale tylko przy wejściu około 20 MB o rzadkim układzie.
2. Odczyt poza buforem w dekoderze obrazów, wymagający wejścia 64 MB i ponad 2 GB pamięci.
3. Odczyt poza buforem, który pojawiał się tylko przy określonej sekwencji wywołań na dwóch uchwytach do tego samego pliku.
4. Ponowne odkrycie CVE-2026-56132 w libexpat (wymagało głęboko zagnieżdżonego wejścia).
5. Błąd logiczny: funkcja ograniczająca dostęp do plików nie zawsze działała, choć nic się nie wysypywało.

Do tego trzy dodatkowe eksperymenty. Claude napisał formalną specyfikację RFC 1950 i udowodnił na binariach x86, że zlib z jądra Linuksa ją poprawnie implementuje. Zbudował też w Ruście interpreter podzbioru Pythona, który w 1,7 mln losowych programów zachował się jak CPython w 99,95% przypadków. A próba weryfikacji popularnego czytnika PDF znalazła w tydzień tyle błędów bezpieczeństwa, ile zwykle zgłasza się w rok.

To ten sam kierunek co przy PHP2Shell i Claude Mythos w Bank of America: modele AI znajdują błędy, których ludzie i klasyczne narzędzia nie wyłapały przez lata. Tyle że tym razem kończy się to nie tylko łatką, ale dowodem.

Na co zwrócić uwagę?

Po pierwsze, na to, co znaczy „zweryfikowany”. Autorzy piszą wprost, że formalna weryfikacja nie oznacza kodu bez błędów (cytując „»Formally verified« does not mean »bug-free.«”). Dowód jest tak dobry jak specyfikacja, modele RISC-V i Linuksa oraz sama sprawdzarka Rocq.

Po drugie, na zakres. Dowody dotyczą statycznych, jednowątkowych binariów RISC-V z musl, a większość z nas uruchamia kod na x86 albo ARM z glibc. Nie obejmują też martwego kodu ani sytuacji, w których to program wywołujący bibliotekę psuje pamięć.

Po trzecie, na koszt. Pojedyncze dowody potrafią pochłonąć setki milionów tokenów, co autorzy sami nazywają głównym ograniczeniem.

Część dowodów jest już na GitHubie (oss-verify-proofs), razem z semantyką RISC-V i Linuksa. Reszta czeka, bo mogłaby ujawnić niezałatane błędy.

FAQ

Co to jest weryfikacja formalna?

To matematyczny dowód, sprawdzony przez program, że kod ma określoną własność dla wszystkich wejść, np. że nigdy nie wykona zapisu poza buforem. Testy i fuzzing sprawdzają tylko wybrane przypadki.

Czy zweryfikowane biblioteki są wolne od błędów?

Nie. Dowód gwarantuje brak awarii tylko w opisanym modelu (RISC-V, Linux, wejście poniżej 64 MB, jeden wątek). Błędy mogą siedzieć w specyfikacji, w modelu maszyny albo poza tym zakresem.

Czy mogę zweryfikować swój projekt?

Theorem prowadzi OSS Verify, bezpłatny program dla wybranych projektów open source. Zgłasza go opiekun projektu przez pull request z plikami project.yaml, Dockerfile i build.sh, podobnie jak w OSS-Fuzz. Trzeba się liczyć z przeniesieniem builda na statyczne binaria riscv64.