Weryfikacja formalna, czyli matematyczny dowód zachowania programu, dotąd wymagała lat pracy ekspertów, a Anthropic i firma Theorem pokazali, że jeden jej rodzaj model AI potrafi już robić hurtowo na prawdziwym oprogramowaniu. Według badania opublikowanego 22 października 2026 roku Claude w kilka tygodni objął dowodami 239 punktów wejścia w 123 bibliotekach z projektu OSS-Fuzz. W części przypadków dowód powstał dopiero po załataniu znalezionych błędów. Żaden z tych punktów nie wywraca się na wejściu mniejszym niż 64 MB. Dowody dotyczą skompilowanego kodu maszynowego dla procesorów RISC-V, a sprawdzał je automat w narzędziu Rocq. Przy okazji wyszły na jaw błędy, których latami nie złapały testy. Autorzy od razu zastrzegają, że “formally verified” nie znaczy “bug-free”, więc ważne jest też to, czego te dowody nie obejmują.
Czym jest weryfikacja formalna i czym różni się od testów
Weryfikacja formalna to matematyczny dowód, że program spełnia ściśle zapisaną regułę dla wszystkich możliwych danych wejściowych w określonym zakresie. Test sprawdza tylko te przypadki, które ktoś wymyślił i uruchomił.
Najbliższa analogia to most. Testy to przejazd kilkoma ciężarówkami: wiemy, że te ciężarówki przejechały. Fuzzing przypomina puszczanie przez most milionów losowych pojazdów przez całą dobę. Znajdzie dużo słabych miejsc, ale nigdy nie sprawdzi wszystkich kombinacji. Dowód to obliczenie konstruktora, które pokazuje, że most uniesie każdy ładunek do zadanej masy. Pod jednym warunkiem: że model materiałów i gruntu w obliczeniach zgadza się z rzeczywistością.
Fuzzing jest dziś standardem w bezpieczeństwie. Program zwany fuzzerem generuje ogromne ilości półlosowych, przerabianych danych i podaje je do kodu, aż coś się wywróci. Anthropic zauważa, że fuzzery zwykle mutują małe wejścia, najczęściej do 1 MB. Błąd, który pojawia się dopiero przy pliku 20 MB o nietypowym układzie, może więc nie wyjść nigdy.
Co dokładnie zrobili Anthropic i Theorem
Zespół wziął gotowe testy fuzzingowe z OSS-Fuzz, czyli projektu Google, który bez przerwy testuje ważne biblioteki open source. Każdy taki test ma punkt wejścia: miejsce, przez które fuzzer podaje dane do kodu. Program jest dodatkowo uzbrojony w AddressSanitizer, narzędzie, które przerywa jego działanie, gdy wykryje niepoprawny dostęp do pamięci.
Z tego powstała reguła do udowodnienia: ten test nie wywróci się dla żadnego wejścia mniejszego niż 64 MB. Bibliotekę razem z testem skompilowano do pliku wykonywalnego na RISC-V. Formalne modele procesora RISC-V i procesu w Linuksie dostarczyła firma Theorem. Claude pisał dowód, a jądro Rocq, programu do sprawdzania dowodów matematycznych, weryfikowało go względem specyfikacji.
Kiedy dowód się nie domykał, często oznaczało to prawdziwy błąd. Claude łatał wtedy kod, specyfikacja powstawała na nowo i dowodzenie ruszało od początku. Autorzy przyznają w przypisie, że to otwiera drogę do oszukiwania nagrody: model mógłby przepisać program tak, żeby trywialnie nigdy się nie wywracał. Dlatego karali każdą łatkę, nagradzali dowód, że zmienia ona niewiele wejść, i przeglądali poprawki pod tym kątem.
Skala: 180 milionów linii dowodów
Gotowe dowody dla 239 punktów wejścia liczą około 180 mln linii w języku Rocq. Typowy dowód ma około 600 tys. linii, a plik wykonywalny, którego dotyczy, to w medianie 18 tys. instrukcji RISC-V. Według dodatku do badania Claude napisał po drodze około miliarda linii, z czego do zatwierdzonych dowodów weszło 180 mln.
Dowody są tak duże, bo obejmują cały proces, a nie tylko bibliotekę: start programu w C, alokator pamięci, printf i środowisko AddressSanitizera. Przykład z dodatku: parser biblioteki cJSON ma 391 linii, a jego dowód 630 tys. linii. Człowiek nie musi tego czytać. Sprawdzenie jednego dowodu przez automat trwa od 30 minut do kilku godzin pracy procesora.
Agenci AI · Kodożercy
Zbuduj sobie dział cyfrowych pracowników
Kurs Agenci AI od Kodożerców przeprowadza krok po kroku przez budowanie agentów w n8n. Pięciu agentów, pięć realnych zadań, a przy każdym wariant przeniesienia rozwiązania na Twój własny przypadek.
Sprawdź kurs Agenci AI →
Jakie błędy Claude znalazł przy dowodzeniu
Próby dowodzenia ujawniły setki błędów, w tym takie, na które fuzzer najpewniej by nie trafił. Anthropic pisze wprost: “Claude also discovered bugs that had eluded detection for years, despite trillions of test runs”. Firma nie podaje nazw większości bibliotek, więc poniżej są tylko przypadki opisane w badaniu.
- Dekompresor: licznik schodził poniżej zera i prowadził do zapisu poza przydzieloną pamięcią, ale tylko przy wejściu około 20 MB o jednym rzadkim układzie.
- Dekoder obrazów: odczyt poza zakresem pamięci wymagał wejścia 64 MB i ponad 2 GB pamięci.
- Obsługa plików: inny odczyt poza zakresem wymagał konkretnej sekwencji wywołań na dwóch uchwytach do tego samego pliku.
- libexpat: Claude ponownie odkrył znaną już podatność CVE-2026-56132, która wymagała głęboko zagnieżdżonych danych.
- Błąd logiczny bez awarii: funkcja ograniczająca, jakie pliki może wczytać aplikacja, nie zawsze działała.
Osobne próby weryfikacji w kilku szeroko używanych aplikacjach dały błąd logiczny ukryty ponad dekadę. Przy czytniku PDF zespół znalazł w tydzień tyle błędów bezpieczeństwa, ile zwykle zgłasza się w rok.
Część pracy kończyła się dowodem własności, a nie błędem. W bibliotece cpp-httplib Claude musiał wykluczyć przepełnienie stosu przy usuwaniu struktury std::set. Udowodnił więc na kodzie maszynowym, że drzewo czerwono-czarne z biblioteki libc++ zachowuje logarytmiczną głębokość. Dodatek opisuje też eksperyment kontrolny z interpreterem Pythona: z siedmiu celowo wstrzykniętych błędów pięć przeszło przez losowe testy, a wszystkie siedem zablokowało dowód.
Czego dowód formalny nie gwarantuje
Dowód gwarantuje tylko to, co zapisano w twierdzeniu, i tylko w świecie opisanym przez model maszyny. Autorzy wymieniają konkretne luki:
- Inna maszyna niż u użytkowników. Dowody dotyczą jednowątkowych, statycznie linkowanych plików RISC-V z biblioteką musl i ze stałym limitem pamięci. Te same biblioteki działają zwykle na x86 albo ARM, dynamicznie linkowane z glibc.
- Wąska reguła. Udowodniono brak awarii dla wejść mniejszych niż 64 MB (w dodatku: 64 MiB) i tylko w wybranych punktach wejścia. AddressSanitizer nie wykrywa wszystkich błędów pamięci, a nawet komplet punktów wejścia nie obejmuje całej biblioteki.
- Odpowiedzialność wywołującego. Program, który źle używa biblioteki, nadal może zepsuć sobie pamięć. Zamknięcie tej luki wymaga opisania, co wywołujący musi robić przy każdej publicznej funkcji.
- Zaufane elementy. Trzeba ufać modelom RISC-V i Linuksa, treści twierdzeń oraz sprawdzarce Rocq. Przypis dokłada do tej listy sprzęt, system i kompilator OCaml, na którym działa Rocq.
Ten ostatni punkt to też zaleta. Błędu szuka się w kilku zaufanych elementach, a nie w milionach linii kodu, i te elementy nie rosną, gdy przybywa weryfikowanych projektów.
Ile kosztuje taki dowód i czy będzie taniej
Pojedynczy dowód potrafi zużyć setki milionów tokenów, czyli jednostek tekstu, za które płaci się przy korzystaniu z modelu. Anthropic pokazuje dwa powody, dla których koszt ma spadać. Na zestawie 36 małych zadań z kodu OSS-Fuzz Opus 5.5 udowadnia połowę z nich przy około 40% mniejszej liczbie tokenów niż Opus 5. Kiedy agenci mogli kopiować sobie nawzajem gotowe fragmenty dowodów, zużyli o 17% mniej tokenów niż przy pracy w pojedynkę.
Rachunek zmienia też powtarzalność. Większość każdego dowodu dotyczy kodu wspólnego dla wszystkich programów, na przykład startu środowiska C. Raz udowodnioną bibliotekę można potem wykorzystać w kolejnych dowodach. Według szacunku Theorem 95% kodu maszynowego z pakietów Nix da się zweryfikować do końca 2027 roku za około 134 mln dolarów. Warunek: modele muszą szybko poprawiać się właśnie w tym zadaniu.
Co to znaczy dla firm i programistów w Polsce
Dla większości firm to na razie zmiana po stronie zależności, a nie własnego kodu. Biblioteki z OSS-Fuzz, takie jak libexpat czy zlib, siedzą w aplikacjach webowych, systemach i urządzeniach używanych także w Polsce. Poprawki znalezione przy dowodzeniu trafiają do nich przez zwykłe aktualizacje, więc aktualne zależności są pierwszym krokiem.
Opiekunowie polskich projektów open source mogą zgłosić się do programu OSS Verify firmy Theorem. Jest bezpłatny dla zakwalifikowanych projektów, a zgłoszenie wygląda jak w OSS-Fuzz: pull request z konfiguracją w repozytorium theorem-labs/oss-verify. Projekt musi dać się zbudować jako statyczny plik dla riscv64. Theorem uprzedza, że znaleziska i łatki generują modele AI i nie obiecuje, że przed wysyłką przejrzy je człowiek.
Hasło “zweryfikowane formalnie” w ofercie albo audycie warto rozpisać na trzy pytania. Jaką regułę udowodniono, dla jakiej platformy i jakim elementom trzeba zaufać? Testy i fuzzing zostają, bo sprawdzają rzeczy spoza twierdzenia, na przykład wydajność albo zachowanie na x86. O tym, jak szybko AI znajduje dziś luki, pisaliśmy przy Chrome, który z pomocą AI załatał ponad tysiąc błędów. Dowody w Rocq to druga strona tego wyścigu. Zamiast szukać kolejnej luki, wykluczają wszystkie awarie objęte twierdzeniem dla danego punktu wejścia i modelu maszyny. Ta sama technika, tylko w matematyce, stała za tym, że Claude sformalizował wielkie twierdzenie Fermata w Lean.
FAQ
Czy weryfikacja formalna zastąpi testy?
Nie w najbliższym czasie. Dowód obejmuje tylko regułę zapisaną w twierdzeniu i tylko model maszyny, na którym go przeprowadzono. W badaniu Anthropic był to brak awarii na RISC-V z Linuksem i musl dla wejść mniejszych niż 64 MB. Testy nadal sprawdzają wydajność, inne platformy i zachowanie, którego nikt nie zapisał jako twierdzenia.
Czym jest Rocq?
Rocq to asystent dowodzenia, czyli program, w którym zapisuje się twierdzenia i dowody matematyczne, a jego jądro mechanicznie sprawdza każdy krok. Wcześniej nosił nazwę Coq. W badaniu Anthropic Claude pisał dowody w języku Rocq, a jądro Rocq rozstrzygało, czy dowód naprawdę spełnia specyfikację.
{ aplikacje webowe }Masz pomysł na aplikację? Najpierw go zobacz
Zanim zainwestujesz w pełny system, przygotujemy klikalny prototyp, który pokażesz zespołowi albo klientom. Potem budujemy aplikację webową, która rośnie razem z firmą.
Podsumowanie
Anthropic i Theorem pokazali, że model językowy potrafi w kilka tygodni zautomatyzować jeden rodzaj weryfikacji formalnej na ponad stu prawdziwych bibliotekach. Dla skali: ręczna weryfikacja jądra seL4 zajęła kiedyś 20 osobolat przy dwóch osobolatach samej implementacji. Claude udowodnił brak awarii dla 239 punktów wejścia w 123 bibliotekach. Dowód dotyczy skompilowanego kodu RISC-V i wejść mniejszych niż 64 MB. Po drodze znalazł błędy, których nie wyłapały biliony uruchomień testów. Dowody nie mówią jednak nic o x86, ARM, glibc, wywołujących ani regułach spoza twierdzenia, a koszt w tokenach jest wciąż wysoki. Część dowodów i modele RISC-V oraz Linuksa są publiczne, więc każdy może je sprawdzić. Firmy najszybciej odczują to przez poprawki w zależnościach, które warto po prostu aktualizować.
Newsletter · DevstockAcademy & Kodożercy
Bądź na bieżąco ze światem IT, AI i automatyzacji
Co wtorek: newsy z branży, praktyczne tipy i narzędzia które warto znać. Zero spamu.
