AlphaProof Code udowodnił poprawność kryptografii Signala — na poziomie skompilowanego pliku binarnego

Sześć i pół miliona linii Lean, wygenerowanych w ciągu czterech tygodni przez zespoły agentów, którym przy pisaniu nie pomógł żaden człowiek. To liczba z nagłówka, którą Google DeepMind opublikował 10 listopada 2026 r. dla AlphaProof Code — agentowego frameworka do weryfikacji formalnej, którego laboratorium użyło do maszynowego sprawdzenia kryptograficznego rdzenia protokołu Signal — i, co nietypowe, do sprawdzenia go na poziomie skompilowanego pliku binarnego AArch64, a nie dokumentu projektowego stojącego ponad nim. Modele, które wykonały tę pracę, to osobna kwestia. jeden klucz API w cenie katalogowej dostawcy z 0% narzutu Silnik agentów dowodzących nie jest czymś, co udostępniamy.

Ten framework nie jest modelem, który można wywołać. To otoczka: ludzcy eksperci decydują, co musi być prawdą, mieszanka modeli zamienia te cele w specyfikacje Lean, a następnie zespoły agentów piszących dowody — blog wymienia Gemini Carbon jako silnik — uzupełniają dowody, aż jądro Lean je zaakceptuje. To, co ukazało się wraz z ogłoszeniem, to zestaw artefaktów pod github.com/google-deepmind/code-verification oraz artykuł techniczny, który znacznie szczerzej niż wpis na blogu mówi o granicach wyniku. Większość tego, co następuje, pochodzi z tego artykułu, ponieważ to w nim znajdują się interesujące liczby.

Co zostało faktycznie udowodnione i przeciwko czemu

Celem jest libsignal v0.105.4 ze spqr v1.6.0, zbudowany standardowym rustc 1.98.1, statycznie zlinkowany z musl i wygenerowany jako pojedynczy plik wykonywalny AArch64 dla Linuksa. Ten szczegół ma większe znaczenie niż jakikolwiek benchmark: dowody dotyczą bajtów, które działałyby na telefonie, a nie funkcji Rusta, którą kompilator ma wiernie przetłumaczyć. Zespół zweryfikował około 560 KB kodu źródłowego libsignal, około 140 000 instrukcji AArch64, i zrobił to, pisząc model Lean zestawu instrukcji — 467 instrukcji i 31 wywołań systemowych w 7578 wierszach — a następnie dowodząc, że rzeczywisty obraz ELF, załadowany i wykonany w ramach tego modelu, zachowuje właściwości bezpieczeństwa.

Właściwości są takie, jakich oczekiwałby inżynier protokołów. Dziesięć twierdzeń symbolicznych obejmuje utajnianie przekazywania dalej, bezpieczeństwo po kompromitacji, tajność inicjatora i respondenta, uwierzytelnianie oraz pięć wniosków z Twierdzenia 1 PQXDH. Główny wynik nosi nazwę signal_session_secure_placed. Istnieje również ścieżka obliczeniowa z konkretnym ograniczeniem, a obie ścieżki używają różnych modeli przeciwnika: strona symboliczna (Dolev–Yao, za pośrednictwem frameworka DyLean) obejmuje nawet atakującego kwantowego, który łamie Diffie–Hellman po handshake'u, podczas gdy strona obliczeniowa obejmuje wyłącznie klasycznych przeciwników.

Dokąd trafia sześć milionów linii

„Ponad sześć milionów linii” to sformułowanie z bloga; jest trafne, ale zgrubne. Przydatne jest zestawienie z pracy — warto je czytać jako tabelę kosztów, a nie popisówkę:

• Dowody dla pliku binarnego — 5,3 miliona linii, większość pracy, obejmujące semantykę kodu maszynowego i rafinację od modelu symbolicznego aż po plik wykonywalny.

• Dowody obliczeniowe — około 860 000 wierszy.

• Dowody symboliczne — około 350 000 linii.

Dowody obalające błędy — około 140 000 linii, dotyczące dwóch celowo ponownie wprowadzonych luk bezpieczeństwa opisanych poniżej.

• Dowody alokatora — około 70 000 wierszy.

Prawie siedem milionów linii, jeśli liczyć komentarze i puste linie – co robi artykuł, a blog nie. Tak czy inaczej, istotny jest stosunek między dowodem a tym, co zostało dowiedzione: 6,5 miliona linii Lean, by ustalić właściwości binarki o rozmiarze 560 KB. Ten stosunek jest uczciwą miarą tego, jak daleko tej technice do rutyny, i to jest liczba, którą warto cytować, gdy ktoś pyta, czy weryfikacja formalna stała się tania.

Zaufana podstawa jest mniejsza niż dowód — i o to właśnie chodzi.

Dowód jest tyle wart, ile jego założenia. Artykuł jest w tej kwestii konkretny, a ta konkretność odróżnia go od komunikatu prasowego. Zaufane specyfikacje mają około 18 000 linii (28 000 wraz z dokumentacją), semantyka AArch64 około 8 000, a kodowanie kodu maszynowego w Lean około 95 000. Trzydzieści siedem procedur zastępuje się kontraktami, zamiast je weryfikować — kompresja SHA-256 i SHA-512, AES-256-CBC, X25519, operacje na krzywych Edwardsa, Kyber1024 i ML-KEM-768 oraz HMAC z libcrux. Osiemnaście punktów wejścia panic również przyjęto jako założenia, zamiast ich dowodzić.

Zatem twierdzenie nie brzmi: „wszystko jest udowodnione”. Twierdzenie jest takie, że logika protokołu kryptograficznego, maszyna stanów sesji oraz rafinacja od tej logiki do faktycznie wykonywanych instrukcji są udowodnione, natomiast leżące u podstaw prymitywy są obdarzane zaufaniem tak, jak każde przedsięwzięcie weryfikacyjne obdarza zaufaniem swoje prymitywy. Kompilator Rust, co istotne, nie znajduje się w zaufanej bazie — zespół uniknął konieczności zaufania mu, rozumując na poziomie kodu maszynowego, co jest tym samym trikiem, który pozwala zespołowi całkowicie obejść się bez zweryfikowanego kompilatora. W kontekście skali artykuł podaje seL4 na około 20 osobolat, a CompCert na około 6.

Dwa błędy, celowo przywrócone

System weryfikacji, który zawsze mówi tylko „poprawny”, jest niemożliwy do przetestowania. Dlatego zespół wziął dwie luki, które wcześniej znaleziono i naprawiono w kodzie Signala — błąd słabego stanu i błąd małej podgrupy — ponownie wprowadził je do izolowanej kopii i ponownie uruchomił potok. W obu przypadkach AlphaProof Code wygenerował sprawdzony maszynowo dowód, że wadliwa wersja nie spełnia twierdzenia bezpieczeństwa: zdanie symboliczne redukuje się do ¬Sec(Asm_bug).

Artykuł dodaje zastrzeżenie, które strona marketingowa by wycięła: obalenie obliczeniowego twierdzenia dla tych błędów jest „znacznie trudniejsze”, a kwestię pozostawiono otwartą. Innymi słowy, test negatywny działa czysto na torze symbolicznym, a jeszcze nie działa na torze obliczeniowym. To dokładnie taki rodzaj asymetrii, o którym czytelnik powinien wiedzieć, zanim zacznie traktować ten framework jako detektor błędów.

Jak uruchamiano agentów

Pięciu badaczy przez cztery tygodnie, każdy bez przerwy uruchamiał agentów. Samo pisanie dowodów wykonywały zespoły liczące od 40 do 80 agentów, działające od 24 do 72 godzin na jednej maszynie na zespół, z agentem nadzorującym ponad orkiestratorem zespołu. Agent-kontroler sprawdza każde zgłoszenie za pomocą komparatora wobec wydzielonej kopii specyfikacji i wobec jądra Lean — środek obrony przed tym, aby agent dowiódł subtelnie osłabionej wersji tego, o co proszono.

Praca ludzka została z góry skoncentrowana na specyfikacjach. Każda specyfikacja została sprawdzona przez eksperta, zanim rozpoczęto prace nad dowodami, a własny przebieg audytu agentów oznaczył około 1% bazy kodu jako wymagający uwagi człowieka. Żaden człowiek nie napisał kodu dowodowego. Artykuł jest również bez ogródek co do inżynierii: czysta kompilacja może zająć kilka godzin, na wczesnym etapie drobna edycja źródła lub ponownie skompilowany plik binarny wymuszały duże naprawy dowodów, a zarówno w dowodach generowanych przez AI, jak i w samych technikach dowodowych istnieje „znaczne pole do optymalizacji”.

Czego nie obejmują dowody

Ograniczenia są na tyle obszerne, że stanowią najważniejszą sekcję artykułu, i są przedstawione wprost. Nie ustalono żadnej gwarancji postkwantowej dla właściwości uzdrawiania SPQR — twierdzenia dotyczące ratchetu zakładają, że atakujący wybiera klucze SPQR. Prywatność ładunku nie jest udowodniona. Uwierzytelnianie respondenta nie jest udowodnione dla pierwszej wiadomości uzgadniania, które nigdy nie zostaje promowane. Model dopuszcza jedną sesję na promocję, stałe długości wiadomości, brak stanu wielourządzeniowego oraz klucze tożsamości oparte na zaufaniu przy pierwszym użyciu.

Istnieje również oszacowanie, które staje się puste. Składnik fałszowania 8-bajtowego MAC wynosi co najmniej 2⁻⁶⁴ na próbę i rośnie kwadratowo wraz z liczbą wiadomości i epok, co oznacza, że oszacowanie przestaje cokolwiek mówić dla pojedynczej sesji obejmującej około 25 000 wiadomości albo dla 2²⁰ sesji po 2¹⁰ wiadomości. A przedmiotem dowodu jest zbudowana przez zespół wersja libsignal-cli uruchamiana jako świeży proces — a nie aplikacja Signal na telefonie. Kilka założeń dotyczących środowiska jest uzasadnianych nieformalnie, a nie dowodzonych.

Nie ma żadnego API, żadnej ceny ani modelu, do którego można by się zwrócić

To jest część, która rozczaruje każdego, kto przychodzi z rankingu modeli. AlphaProof Code to framework badawczy i opublikowany zestaw artefaktów. Nie ma endpointu, cennika za token, listy oczekujących ani wag: repozytorium zawiera rozwój w Lean, semantykę AArch64, binding libsignal i specyfikacje, a nie checkpoint. Blog mówi, że artefakty są udostępnione jako open source; strona docelowa nie podaje licencji, co warto sprawdzić, zanim ktokolwiek planuje na nich budować.

Modele, które wykonały tę pracę, to osobna kwestia. W artykule wskazano G​emini 4 Carbon jako model używany przez agentów dowodzących i podano, że Claude Opus 5.5 był używany wraz z innymi modelami do sporządzania i przeglądu specyfikacji. Claude Opus 5.5 jest dziś w katalogu OrcaRouter po 4 USD za milion tokenów wejściowych i 20 USD za milion tokenów wyjściowych, a cena katalogowa dostawcy jest przekazywana bez marży (0%) — więc jeśli praktycznym wnioskiem, który chcesz wyciągnąć, jest „uruchomienie pętli tworzenia specyfikacji z modelem użytym w artykule”, to ta część jest zwykłym wywołaniem API, a zmiana ceny przez dostawcę jest odzwierciedlana po naszej stronie tego samego dnia. Nie udostępniamy silnika agentów dowodzących i nic tutaj nie sugeruje, że hostujemy sam AlphaProof Code.

Dlaczego to jest większa sprawa niż wynik Signal

Weryfikacja Signala jest imponująca sama w sobie — to pierwsza formalna weryfikacja szeroko wdrożonego protokołu, a konkretnie jego implementacji dowolną metodą, z AI lub bez niej, według DeepMind, oraz pierwszy raz, gdy AI zweryfikowała wdrożony protokół kryptograficzny na takim poziomie szczegółowości. Ale przenośna konkluzja dotyczy przepływu pracy. Zespół pięciu osób w cztery tygodnie, z etapem przeglądu specyfikacji i agentem pełniącym rolę strażnika, wytworzył korpus dowodów, który wcześniej byłby projektem wieloletnim. Jeśli ta proporcja utrzyma się choćby luźno, zmienia się zbiór systemów, na które stać weryfikację: firmware urządzeń medycznych, oprogramowanie sieci energetycznych, ten rodzaj kodu, który obecnie dostaje przegląd kodu i modlitwę.

Czy to się utrzymuje, pozostaje niesprawdzone. Kryptografia Signala jest niezwykle dobrze wyspecyfikowana, zespół poprosił własnych inżynierów Signala o przegląd metodologii, a prymitywy zlecono na zewnątrz, zamiast je zweryfikować. Kolejny system nie będzie tak ustępliwy. Sposób, w jaki sama praca ujmuje temat — połączenie weryfikacji formalnej z automatycznymi agentami obronnymi takimi jak CodeMender — to uczciwy kształt tej propozycji: weryfikacja mówi, co jest prawdą, a coś innego musi naprawić to, co nią nie jest.

Co obejrzeć

Trzy rzeczy przeniosłyby to z przełomowego artykułu do techniki przemysłowej. Druga, niezależna baza kodu zweryfikowana przez kogoś spoza Google, najlepiej taka, w której specyfikację trzeba było napisać od zera, a nie zaadaptować z istniejącej analizy. Wskaźnik kosztów — godziny agenta, godziny akceleratora, dolary — ponieważ cztery tygodnie i zespoły liczące od 40 do 80 agentów to jednostka, według której żaden menedżer inżynierii nie może planować budżetu. Oraz obalanie błędów na ścieżce obliczeniowej, które artykuł pozostawia otwarte i które stanowi różnicę między systemem, który dowodzi właściwości, a systemem, który potrafi także powiedzieć — obliczeniowo — że konkretny plik binarny jest błędny.

Do tego czasu czytaj repozytorium artefaktów, a nie ogłoszenie. Dowody są tam, Lean je sprawdza, a artykuł dokładnie mówi, jakie przyjmuje założenia.