Il 10 novembre 2026 Google DeepMind ha annunciato di aver usato il suo nuovo framework di IA, AlphaProof Code, per verificare formalmente il codice effettivo del protocollo Signal. La verifica formale consiste nel dimostrare matematicamente che un software si comporta esattamente come previsto, senza bug nascosti. Il team ha guidato agenti di IA nella generazione e nel controllo di una dimostrazione che attesta come il codice compilato di Signal rispetti importanti garanzie di sicurezza, per esempio mantenere al sicuro i messaggi anche se un dispositivo viene temporaneamente compromesso. Il lavoro è durato quattro settimane, mentre normalmente un compito del genere richiederebbe anni a team di esperti.
Cosa fa AlphaProof Code
AlphaProof Code è un sistema agentico basato su più LLM (modelli linguistici di grandi dimensioni). I ricercatori umani traducono prima gli obiettivi di sicurezza di Signal in specifiche formali, verificando ogni passaggio. Poi un gruppo di agenti, basati sul modello Gemini Carbon di DeepMind, scrive la dimostrazione in Lean, un linguaggio che verifica i teoremi matematici. Gli agenti hanno generato oltre sei milioni di righe di codice Lean e segnalato per la revisione umana solo circa l’uno per cento del codice. Il sistema ha anche individuato correttamente due bug già risolti quando sono stati reintrodotti, dimostrando di saper distinguere il codice sicuro da quello difettoso.
Perché è importante
La verifica riguarda l’implementazione compilata, non soltanto il progetto, colmando una lacuna in cui si nascondono molte vulnerabilità reali. Ehren Kret, responsabile della tecnologia di Signal, ha detto che il risultato offre «maggiore fiducia nelle garanzie di privacy del nostro codice». Gli esperti lo considerano un passo verso l’uso dell’IA per offrire garanzie di sicurezza di alto livello a banche, dispositivi medici, software per reti elettriche e altri sistemi critici.
Perché conta
Per gli utenti di tutti i giorni, il lavoro significa che la crittografia che protegge miliardi di messaggi su Signal e Google Messages è stata verificata matematicamente a livello di implementazione, riducendo il rischio di difetti nascosti. Per gli sviluppatori, dimostra che la verifica formale assistita dall’IA può accelerare concretamente i controlli di sicurezza, anche se non sono ancora chiari i costi e le possibilità di applicarla su scala più ampia.
