AlphaProof Code: Agenci AI napisali trzy miliony linii dowodów, by zweryfikować szyfrowanie Signala

Formalna weryfikacja oprogramowania od dekad pozostaje zajęciem dla cierpliwych: dowodzenie, że kod robi dokładnie to, co deklaruje, wymaga setek godzin pracy ekspertów i zwykle kończy się na wąskim wycinku systemu. Google DeepMind twierdzi, że znalazł sposób, by tę barierę skalować. Zaprezentowany 10 listopada system AlphaProof Code to zestaw agentów opartych na modelach AI, które samodzielnie piszą dowody w asystencie dowodzenia Lean. Efektem ma być trzy miliony linii dowodów wygenerowanych na potrzeby weryfikacji rdzenia kryptograficznego Signala, komunikatora uchodzącego za wzorzec prywatności.

Skala robi wrażenie, ale kluczowa jest tu nie liczba linii, lecz charakter pracy. Lean to język i narzędzie, w którym każdy krok rozumowania musi zostać zaakceptowany przez mechaniczny sprawdzian poprawności, nie ma miejsca na „prawie dobrze”. Agent, który potrafi w takim środowisku działać iteracyjnie, rozbijać cele na podcele i poprawiać własne błędy, adresuje realne wąskie gardło: brak rąk do pracy, a nie brak pomysłów na to, co warto udowodnić. DeepMind pozycjonuje projekt jako dowód, że automatyzacja rozumowania matematycznego przekłada się na praktykę inżynierską.

Wybór Signala nie jest przypadkowy. Protokoły kryptograficzne to obszar, w którym błąd implementacji potrafi zniweczyć cały model bezpieczeństwa, a jednocześnie miejsce, gdzie formalne dowody mają największą wartość, właśnie dlatego, że są tak kosztowne. Jeśli agenci potrafią domykać dowody dla istniejącego, dojrzałego kodu, otwiera to drogę do weryfikacji bibliotek kryptograficznych, systemów operacyjnych czy firmware’u, czyli warstw, których nikt rozsądny nie przepisuje od zera tylko po to, by móc je udowodnić.

Trzeba jednak zachować proporcje. Komunikat firmy to materiał promocyjny, a nie recenzowana publikacja, brakuje w nim szczegółów metodologicznych, informacji o tym, jaka część dowodów wymagała interwencji człowieka, ile z nich dotyczyło właściwości trywialnych, a ile rzeczywistych gwarancji bezpieczeństwa, oraz jak wygląda audyt samego pipeline’u. W świecie formalnej weryfikacji „wygenerowano trzy miliony linii” nie znaczy „udowodniono, że Signal jest bezpieczny”. Znaczy: powstał duży korpus dowodów, który ktoś musi teraz ocenić pod kątem tego, co faktycznie zostało pokazane.

Nie bez znaczenia jest też kontekst rynkowy. DeepMind od lat inwestuje w modele do matematyki i rozumowania, a AlphaProof Code wpisuje się w szerszą narrację: AI nie tylko pisze kod, ale zaczyna go uzasadniać. To subtelna, lecz istotna zmiana akcentów, z generowania prawdopodobnie działających fragmentów na wytwarzanie artefaktów, których poprawność da się sprawdzić maszynowo. Dla branży bezpieczeństwa to potencjalnie najciekawszy kierunek, w jakim zmierza obecna fala agentów.

Pozostaje pytanie o dostępność i koszt. Trzy miliony linii dowodów to także trzy miliony linii, które trzeba utrzymywać przy każdej zmianie w kodzie, a weryfikacja, która nie nadąża za rozwojem oprogramowania, szybko staje się muzealnym eksponatem. Sukces AlphaProof Code zależeć będzie więc nie od jednorazowego wyczynu, lecz od tego, czy agenci potrafią wchodzić w codzienny cykl wytwarzania oprogramowania: tanio, powtarzalnie i w sposób, któremu zespół inżynierów zaufa.

Podsumowanie: AlphaProof Code to ambitna próba przeniesienia automatyzacji rozumowania z matematyki do inżynierii bezpieczeństwa. Trzy miliony linii dowodów w Lean dla szyfrowania Signala brzmi jak kamień milowy, i być może nim jest, ale dopóki nie zobaczymy niezależnej analizy zakresu i kosztów tej weryfikacji, należy traktować go jako obiecujący sygnał, nie jako domknięty dowód.