AlphaProof Code: AI od DeepMind matematicky ověřila kód protokolu Signal

Google DeepMind 10. 11. 2026 oznámil, že výzkumníci s pomocí AI agentů dokázali klíčové bezpečnostní vlastnosti skutečné implementace protokolu Signal, tedy kódu, který chrání soukromé konverzace v aplikaci Signal a v Google Messages. Firmě podle vlastního vyjádření šlo o úlohu, která se v bezpečnosti softwaru dlouho považovala za mimořádně náročnou.

Jde o něco jiného, než když model jen „zkontroluje kód“ a napíše komentář. Formální verifikace znamená, že se vlastnost zapíše jako matematické tvrzení a důkaz zkontroluje stroj – tady důkazní asistent Lean. Když je důkaz v pořádku, Lean ho přijme. Když není, nepřijme ho, i kdyby byl text důkazu stylisticky sebelepší.

Co přesně ověřili – a co ne

Podle oznámení DeepMind jde o první případ, kdy AI formalizovala takto nasazený kryptografický protokol do této hloubky, a také o první formalizaci implementace takto rozšířeného protokolu vůbec, s AI i bez ní.

Důležité je, co se v textu říká a co ne:

• Ověřovali klíčové vlastnosti jádra kryptografického kódu, ne celou aplikaci Signal (rozhraní, servery, instalace v telefonu, zálohy chatů).
• Agenti podle DeepMind dokázali, že zkompilovaný kód splňuje zadané vlastnosti, až na úroveň kódu, který má na zařízeních běžet. Firma zdůrazňuje, že právě mezera mezi návrhem protokolu a jeho implementací bývá zdrojem skutečných chyb.
• Jako příklad vlastností uvedlo oznámení ochranu zpráv předtím, než dojde k dočasnému kompromitování zařízení, i potom. Technická zpráva to rozvádí u implementace libsignal: pokrývá handshake PQXDH a Triple Ratchet a dokládá forward secrecy, autentizaci, bezpečnost po kompromitaci a utajení handshake. V symbolickém modelu uvádí také utajení handshake vůči budoucímu útočníkovi s kvantovým počítačem.
• Technická zpráva připomíná, že varianty protokolu Signal používají i WhatsApp, Messenger a Google Messages. To vysvětluje, proč je protokol důležitý. Neznamená to, že DeepMind ověřil kód těchto dalších aplikací.

Ehren Kret, technický ředitel Signalu, v oznámení uvedl, že přístup umožnil výrazné rozšíření rozsahu oproti dřívější formalizaci menších částí kódu a že mu automatizované převádění živého kódu na platné věty v Lean dává větší jistotu v garance soukromí.

Jak AlphaProof Code pracuje

AlphaProof Code DeepMind popisuje jako víceagentní rámec, který práci rozdělí podobně jako výzkumný tým.

Nejdřív lidé společně s modely převedou bezpečnostní cíle do formálních specifikací. Každou specifikaci podle firmy recenzují lidští odborníci. Teprve potom důkazy provádějí agenti pohánění modelem Gemini Carbon. Oznámení uvádí, že vygenerovali přes šest milionů řádků v jazyce Lean. Technická zpráva je konkrétnější: asi 6,5 milionu strojově zkontrolovaných řádků důkazů, opřených o zhruba 26 tisíc řádků důvěryhodných specifikací a sémantiky architektury AArch64.

Pak agenti důkaz auditovali a označili místa, která si má znovu prohlédnout člověk. Podle DeepMind šlo asi o jedno procento kódu. Zbytek má hlídat sám Lean, takže se odborníci mohou soustředit tam, kde je lidský úsudek nepostradatelný.

Celý tento běh prý trval čtyři týdny. DeepMind to srovnává s tím, že podobná práce historicky zabrala expertním týmům roky. Jde o tvrzení firmy, ne o nezávislé měření.

Aby ověřili, že systém pozná i vadný kód, do izolované verze kódu Signalu znovu vložili dvě dříve opravené chyby. V obou případech systém podle oznámení sestavil strojově zkontrolovaný důkaz, že vadná verze bezpečnostní tvrzení nesplňuje.

Proč na tom záleží, i když to není návod pro každého

Běžný uživatel Signalu nemusí díky tomuto oznámení nic zapínat ani aktualizovat „kvůli AlphaProof“. Jde o výzkumný výsledek, který má posílit jistotu v jádro protokolu, ne o nové tlačítko v aplikaci.

Pro české čtenáře je na tom zajímavé hlavně trojí:

1. U AI už nejde jen o text a obrázky. Tady model nepsal esej o bezpečnosti, ale pomáhal skládat důkazy, které musí projít kontrolou Leanu. Když se splete, důkaz neprojde.
2. Člověk z procesu nevypadl. Specifikace recenzují odborníci a část výstupu znovu čtou. AI tady nenahrazuje odpovědnost za to, co se má dokázat.
3. Souvislost s Gemini 4 Carbon je jiná než v dnešním Rychlém přehledu. Carbon už není jen nový model v ceníku. DeepMind ho v tomto projektu použil jako motor důkazových agentů. To je konkrétní, i když stále laboratorní, použití.

DeepMind zároveň říká, že stejný přístup by jednou mohl pomáhat i u jiných kritických systémů, od firmwaru zdravotnických zařízení po softwaru v energetice. To je výhled firmy, ne hotový produkt. Artefakty formalizace dává k dispozici na google-deepmind.github.io/code-verification.

Co z toho neplyne

• Nevyplývá z toho, že by AI „dokázala, že Signal nelze nabourat“. Ověřené jsou zadané vlastnosti konkrétního kryptografického jádra, ne celý ekosystém aplikace, zařízení a lidí.
• Nevyplývá z toho, že by formalizace nahradila běžné bezpečnostní audity, odměny za chyby ani aktualizace.
• Čísla o šesti milionech řádků, čtyřech týdnech a jednom procentu k recenzi pocházejí od DeepMind. Neověřovali jsme je vlastním během.

Údaje v článku jsme ověřili k 11. 11. 2026 v oznámení Google DeepMind z 10. 11. 2026 a v přiložené technické zprávě.