Google DeepMind ha presentato il 10 novembre 2026 AlphaProof Code, un sistema che utilizza gruppi coordinati di agenti di intelligenza artificiale per produrre dimostrazioni formali di proprietà di sicurezza direttamente sul codice macchina compilato della libreria crittografica Signal. Il progetto è stato realizzato da cinque ricercatori nell’arco di quattro settimane e riguarda l’implementazione effettiva di componenti utilizzati per la protezione delle comunicazioni, anziché una rappresentazione astratta dei protocolli. Il gruppo ha utilizzato versioni non modificate di libsignal 0.105.4 e SPQR 1.6.0, racchiudendole in un piccolo programma a riga di comando e compilando il risultato con rustc standard in un eseguibile Linux AArch64 collegato staticamente. Le verifiche prodotte sono state espresse nel linguaggio formale Lean, che permette di controllare automaticamente la correttezza delle dimostrazioni rispetto alle specifiche stabilite.
Il processo ha generato circa 6,5 milioni di righe di dimostrazioni Lean controllate automaticamente, costruite sopra circa 26.000 righe di specifiche considerate affidabili e di definizioni semantiche dell’architettura AArch64. I ricercatori hanno utilizzato agenti basati su Gemini 4 Carbon e Claude Opus 5.5 per preparare e revisionare le specifiche, prevedendo anche verifiche effettuate da una famiglia di modelli differente. Successivamente, gruppi di agenti Gemini 4 Carbon hanno generato l’intero codice delle dimostrazioni, senza che gli autori scrivessero manualmente le prove. Le campagne comprendevano normalmente tra 40 e 80 agenti eseguiti sulla stessa macchina per periodi compresi tra 24 e 72 ore. Un orchestratore coordinava responsabili di gruppo, agenti incaricati delle dimostrazioni e componenti dedicati all’integrazione e alla manutenzione della base formale condivisa.
La procedura di accettazione prevedeva due verifiche separate. Il kernel di Lean controllava la validità matematica delle dimostrazioni, mentre un comparatore verificava che le specifiche utilizzate corrispondessero esattamente a quelle approvate dai ricercatori, comprese tutte le definizioni richiamate indirettamente. Gli agenti potevano proporre modifiche alle specifiche quando emergevano difficoltà nelle prove, ma le modifiche alle assunzioni affidabili richiedevano un’autorizzazione umana oppure l’applicazione di politiche preventivamente stabilite. Le modifiche venivano registrate insieme alle relative motivazioni. Questo meccanismo impediva che una dimostrazione venisse accettata semplicemente perché un agente aveva indebolito, anche indirettamente, le condizioni che avrebbe dovuto verificare.
L’analisi ha riguardato il codice delle sessioni individuali utilizzato per l’handshake PQXDH e la messaggistica Triple Ratchet. I ricercatori hanno prodotto dieci teoremi simbolici basati su assunzioni crittografiche idealizzate e una dimostrazione computazionale che limita il vantaggio ottenibile da un attaccante in funzione delle ipotesi crittografiche e di termini statistici. Le proprietà considerate comprendono autenticazione, segretezza delle comunicazioni precedenti alla compromissione dello stato corrente, recupero della sicurezza dopo una compromissione e riservatezza dell’handshake. La verifica simbolica comprende anche la protezione dell’handshake rispetto a una successiva compromissione del meccanismo Diffie–Hellman. Per verificare la capacità delle specifiche di individuare vulnerabilità concrete, il gruppo ha reintrodotto artificialmente due errori già corretti in libsignal, denominati weak state e small subgroup, ricompilando i programmi modificati. In entrambi i casi, il sistema ha prodotto dimostrazioni formali del fallimento delle proprietà simboliche previste. Specifiche, materiali di verifica e istruzioni per ricostruire le dimostrazioni sono stati resi disponibili pubblicamente per consentire controlli indipendenti.
Questo articolo è stato redatto con il supporto di strumenti di intelligenza artificiale (AI)