✨︎ Resumen (TL;DR):
- Google DeepMind usó AlphaProof Code, un sistema de agentes de IA, para verificar formalmente varias garantías criptográficas del protocolo de Signal.
- La prueba duró cuatro semanas y no encontró vulnerabilidades nuevas en las partes examinadas, aunque sí detectó fallas conocidas en versiones antiguas.
- El análisis no cubrió toda la app de Signal; el equipo prevé publicar la especificación y la demostración para que otros equipos las usen.
Investigadores de Google DeepMind usaron AlphaProof Code para verificar formalmente varias garantías criptográficas del protocolo de Signal durante una prueba de cuatro semanas. El análisis no encontró vulnerabilidades nuevas en las partes examinadas, pero no cubrió toda la aplicación de mensajería. El diseño del protocolo también se utiliza en WhatsApp y Google Messages, aunque el reporte no indica que DeepMind haya revisado las implementaciones de esos servicios.
La verificación formal es un método que busca demostrar, mediante razonamiento matemático, que determinadas propiedades se cumplen bajo condiciones definidas. En este caso, DeepMind examinó una parte delimitada del protocolo, no cada función de la aplicación.
El protocolo reúne especificaciones que permiten proteger comunicaciones con cifrado de extremo a extremo. WIRED no detalló cuáles fueron las garantías concretas verificadas ni identificó todos los componentes incluidos en el análisis.
Qué examinó AlphaProof Code
AlphaProof Code es un sistema de agentes de inteligencia artificial que puede contribuir al trabajo y corregirse durante varias etapas. Según WIRED, los investigadores mantuvieron intervención humana en momentos clave mientras desarrollaban el análisis.
El equipo puso la herramienta a prueba con versiones antiguas de Signal que contenían vulnerabilidades conocidas y ya corregidas. En esos casos, AlphaProof Code identificó las fallas y mostró que las versiones afectadas no podían superar la verificación planteada.
Los investigadores prevén publicar la especificación y la demostración que desarrollaron para que otros equipos puedan usarlas. También reconocieron que su trabajo partió de análisis formales anteriores de Signal Foundation.
Ehren Kret, director de tecnología de Signal, dijo en una declaración recogida por WIRED que el método de DeepMind permite ampliar las verificaciones previas y da más confianza en las garantías de privacidad del código.
Qué demuestra una verificación formal
Una especificación describe con precisión lo que se espera de una parte del software. La demostración comprueba una afirmación concreta respecto de esa descripción y de los supuestos utilizados.
Si una función, un componente o una condición queda fuera del análisis, la conclusión no cubre automáticamente ese elemento. Por eso, la ausencia de fallas nuevas en los fragmentos examinados refuerza la confianza en las garantías revisadas, pero no equivale a una evaluación completa de todas las funciones de Signal.
El Instituto Nacional de Estándares y Tecnología de Estados Unidos (NIST) advierte que, incluso cuando existen pruebas formales, siguen siendo necesarias otras pruebas. Los supuestos de una demostración pueden no cumplirse cuando una especificación se traslada al código implementado.
Signal ya había verificado partes de su código
En 2025, Signal informó que había verificado formalmente el código de SPQR, un componente añadido al protocolo para reforzar su resistencia frente a futuros ataques con computadoras cuánticas. El artículo de WIRED no precisa si ese componente está entre los que examinó DeepMind.
Otro esfuerzo, Signal Shot, busca verificar de manera más amplia el protocolo y la aplicación de Signal con el asistente de demostraciones Lean. La Beneficial AI Foundation, Signal y Lean FRO lanzaron el proyecto en abril de 2026.
Sus objetivos describen un trabajo más amplio, pero no establecen por sí solos qué partes cubrió la prueba de AlphaProof Code.
Cuatro semanas no revelan el costo de repetirlo
DeepMind realizó el análisis como un proyecto de investigación sin cobrar por él, según WIRED. Google no reveló cuánto costó ni si planea ofrecer un servicio comercial.
Las cuatro semanas describen la duración de esta prueba, pero no permiten calcular cuánto costaría aplicar el proceso a otros programas.
El resultado deja una conclusión acotada: AlphaProof Code no encontró vulnerabilidades nuevas en las partes examinadas, mientras que sí detectó fallas conocidas en versiones antiguas. La revisión suma evidencia a análisis formales previos, pero la aplicación completa de Signal y las implementaciones de WhatsApp y Google Messages quedan fuera de lo que esta prueba permite afirmar. La especificación y la demostración anunciadas serán los materiales que otros equipos podrán revisar cuando se publiquen.
