DeepMind: agenci AI w cztery tygodnie udowodnili własności bezpieczeństwa kodu protokołu Signal

Google DeepMind ogłosiło 10 listopada 2026 roku, że za pomocą agentów AI formalnie zweryfikowało kluczowe własności bezpieczeństwa kodu stojącego za protokołem Signal. Według firmy dowody dotyczą skompilowanego kodu działającego na urządzeniach, a nie tylko założeń projektowych protokołu.

Co udowodniono

Protokół Signal jest używany w aplikacji Signal i w Google Messages, a według 9to5Mac korzysta z niego także WhatsApp. DeepMind podaje, że agenci udowodnili między innymi ochronę wiadomości przed i po tymczasowym przejęciu urządzenia.

Weryfikacja formalna oznacza matematyczne dowodzenie, że protokół spełnia założenia bezpieczeństwa. To wyższy poprzeczka niż zwykłe testy, które szukają błędów, ale nie wykluczają istnienia kolejnych.

Jak działa AlphaProof Code

System nazywa się AlphaProof Code i jest wieloagentowym frameworkiem oparzonym na wielu modelach językowych, który dzieli pracę między ludzi i AI. Badacze z pomocą mieszanki modeli przełożyli cele bezpieczeństwa Signala na formalne specyfikacje, a każdą z nich przejrzeli eksperci.

Dowody w Lean pisali agenci oparci na Gemini Carbon. Następnie agenci audytowali dowody i oznaczali fragmenty wymagające uwagi człowieka. Według DeepMind każdy dowód jest automatycznie sprawdzany przez Lean, co pozwala zweryfikować pracę agentów.

Ograniczenia

DeepMind podaje, że zweryfikowano rdzeń kryptograficzny Signala, i zastrzega, że skalowanie tych technik wymaga dalszych badań. 9to5Mac podkreśla, że weryfikacja dotyczy protokołu, a nie całej aplikacji. Ocena człowieka pozostaje potrzebna przy specyfikacjach i oznaczonych fragmentach dowodów.

Według 9to5Mac proces wymaga dużej mocy obliczeniowej, a Google nie wie, jak praktyczne będzie szersze zastosowanie. Zużytych zasobów nie ujawniono, więc nie należy zakładać, że inne protokoły zostaną szybko zweryfikowane. Firma sama twierdzi, że to pierwsze takie zweryfikowanie wdrożonego protokołu kryptograficznego na tej głębokości z użyciem AI.

Do skalowania tego na całe oprogramowanie świata jest jeszcze daleka droga - Swarat Chaudhuri, naukowiec DeepMind, w rozmowie z WIRED (cyt. za 9to5Mac)

Reakcja Signala i dalsze plany

Dyrektor ds. technologii (CTO) Signala Ehren Kret ocenił, że użycie agentów AI do tłumaczenia działającego kodu na poprawne twierdzenia w Lean to „duży przełom”, a weryfikacja daje „jeszcze większą pewność co do gwarancji prywatności w naszym kodzie”. Rolfe Schmidt, Michael Rosenberg i Kret przekazali uwagi do metodologii.

DeepMind udostępnia artefakty weryfikacji do wykorzystania przez społeczność i wskazuje, że podejście mogłoby objąć inne krytyczne systemy, takie jak oprogramowanie urządzeń medycznych czy sieci energetycznych. To na razie zapowiedź kierunku, nie wdrożenie.