Google DeepMind oznámil, že jeho systém AlphaProof Code matematicky dokázal vybrané bezpečnostné vlastnosti skutočného kódu, ktorý chráni súkromné správy miliárd ľudí. Je to významný krok, no slogan „koniec softvérovým chybám“ by bol predčasný. Tu je, čo sa naozaj podarilo a čo nie.
Čo DeepMind oznámil
Dňa 10. novembra 2026 Google DeepMind uviedol, že výskumníci použili agentný systém AlphaProof Code na formálne overenie kľúčových kryptografických záruk protokolu používaného v komunikačnej aplikácii Signal. Ide o šifrovací protokol, ktorý v upravenej podobe chráni aj ďalšie veľké komunikačné služby. Projekt trval štyri týždne a podľa DeepMindu išlo o výskumnú spoluprácu bez poplatku.
Zásadná je hĺbka overenia: nie len návrh protokolu na papieri, ale podľa DeepMindu aj skutočný implementačný kód, až po úroveň skompilovaného strojového kódu. Väčšina predchádzajúcich prác sa zastavila pri architektúre alebo pri menších častiach kódu. DeepMind tvrdí, že ide o prvé overenie takto rozšírenej implementácie protokolu AI systémom a zverejnil technický článok aj podkladové artefakty.
Čo je formálna verifikácia (a čím sa líši od testovania)
Pri testovaní skúšate, či program funguje pre vybrané vstupy. Čo ste nevyskúšali, to nevidíte. Pri formálnej verifikácii matematicky dokazujete, že program spĺňa vopred zapísanú požiadavku pre všetky možné vstupy. Dôkaz sa zapisuje v jazyku, ktorý kontroluje špeciálny program, takže správnosť dôkazu nemusí posudzovať človek.
Je to ako rozdiel medzi vyskúšaním mosta niekoľkými nákladiakmi a matematickým výpočtom, že unesie akékoľvek zaťaženie do určitej hranice. Výpočet však platí len za predpokladov, ktoré do neho vložíte.
Ako to AlphaProof Code urobil
- Ľudia a modely najprv zapísali, čo má platiť. Ciele protokolu preložili do matematických špecifikácií a každú z nich skontrolovali ľudskí experti ešte pred spustením dôkazov.
- Agenti potom vytvárali dôkazy. Systém vygeneroval viac než 6 miliónov riadkov dôkazu v jazyku určenom na strojovú kontrolu.
- Ľudia kontrolovali len malú časť. Podľa DeepMindu agenti označili približne jedno percento kódu na opätovnú ľudskú kontrolu.
- Dôkazy sa týkajú aj situácií po napadnutí. Zahŕňajú ochranu súkromia pred dočasným prelomením zariadenia a po ňom.
Dôležitý kontrolný test: keď systém spustili na starších verziách s už opravenými zraniteľnosťami, tieto chyby našiel a ukázal, že tieto verzie sa overiť nedajú. Overovač teda zlý kód nepustí, čo je presne to, čo od neho čakáme.
Čo to nie je
- Nie je to dôkaz, že „Signal je dokonale bezpečný“. Overené boli vybrané vlastnosti jadra kryptografického kódu za stanovených predpokladov, nie celá aplikácia ani všetky spôsoby, ako môže zlyhať.
- Nie je to „stopercentná“ istota o softvéri. Dôkaz je len taký dobrý ako špecifikácia. Ak je požiadavka zapísaná nesprávne alebo neúplne, program môže matematicky spĺňať niečo, čo nikto nechcel.
- Nie je to nástroj, ktorý si dnes stiahne každý vývojár. Ide o výskumný systém a zverejnené artefakty, nie hotový produkt na každodenné použitie.
- V nových vlastnostiach protokolu nenašiel nové chyby. Výskumníci žiadne nové nedostatky v preskúmaných častiach neoznámili. Samotný protokol navyše už roky analyzujú akademici.
Prečo je to dôležité aj tak
Formálna verifikácia sa dlho považovala za príliš drahú a pomalú na široko používaný produkčný kód. Ak AI agenti dokážu vytvoriť strojovo overené dôkazy pre reálnu implementáciu za týždne, ťažisko práce sa presúva: z písania dôkazov na písanie presných špecifikácií a overovanie predpokladov, na ktorých dôkazy stoja. Inými slovami, kto napíše špecifikáciu, ten v skutočnosti rozhoduje o tom, čo znamená „bezpečné“.
Odborníci zároveň upozorňujú, že otvorená zostáva otázka nákladov: či sa takéto overovanie dá škálovať aj mimo mimoriadne kritického kódu, ako sú šifrovacie knižnice.
Čo z toho plynie pre vývojárov
- Formálna verifikácia sa pravdepodobne najskôr rozšíri tam, kde je cena chyby vysoká: kryptografia, protokoly, jadrá operačných systémov, zdravotnícky a dopravný softvér.
- Pre bežný webový alebo mobilný vývoj zostávajú základom testy, kontroly kódu, bezpečné nastavenia a aktualizácie. Formálny dôkaz ich nenahrádza.
- Naučiť sa písať jasné požiadavky (čo presne musí platiť, a čo nikdy nesmie nastať) je užitočné aj bez dôkazov.
Zhrnutie
AlphaProof Code ukázal, že AI dokáže spolupracovať s ľuďmi na strojovom overení reálneho kryptografického kódu v rozsahu, ktorý bol donedávna prakticky nedosiahnuteľný. To je skutočný míľnik. Neznamená však koniec softvérových chýb, lebo dôkaz hovorí len o tom, čo sme sa rozhodli zapísať, a ostatné vrstvy systému zostávajú na ľuďoch. Dobrá správa je, že overenie sa mení z akademického luxusu na niečo, čo sa dá robiť v rozumnom čase. A to stojí za sledovanie.
