Investigadores de Google DeepMind usaron AlphaProof Code, un sistema de agentes de inteligencia artificial, para verificar formalmente varias garantías criptográficas del protocolo de Signal en una prueba de cuatro semanas, informó WIRED. El análisis no encontró vulnerabilidades nuevas en las partes examinadas, pero no abarcó toda la aplicación de mensajería.
El protocolo reúne especificaciones que permiten proteger comunicaciones con cifrado de extremo a extremo. Además de Signal, su diseño se utiliza en servicios como WhatsApp y Google Messages. El resultado aporta una revisión adicional de parte de esa tecnología, aunque el reportaje no indica que el equipo haya examinado las implementaciones de esas otras aplicaciones.
Qué examinó AlphaProof Code
La verificación formal busca demostrar con razonamiento matemático que determinadas propiedades se cumplen bajo unas condiciones definidas. AlphaProof Code ayudó a los investigadores de DeepMind a desarrollar ese trabajo mediante agentes de IA que pueden contribuir y corregirse durante varias etapas, con intervención humana en momentos clave, según WIRED.
El equipo también 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. WIRED no detalla cuáles fueron las garantías concretas verificadas ni identifica todos los componentes incluidos en el análisis.
Ehren Kret, director de tecnología de Signal, dijo en una declaración recogida por la revista 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. Los investigadores reconocieron que su trabajo partió de análisis formales anteriores de la Signal Foundation.
Qué significa una demostració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 a esa descripción y a 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.
El Instituto Nacional de Estándares y Tecnología de Estados Unidos, conocido como NIST, advierte que incluso cuando existen pruebas formales siguen siendo necesarias otras pruebas: los supuestos de una demostración pueden no cumplirse al trasladar una especificación al código implementado.
Esa distinción importa para interpretar el resultado de DeepMind. 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 ni elimina la necesidad de seguir revisando el software.
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, tiene la meta más amplia de verificar 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 y no establecen por sí solos qué partes cubrió la prueba de AlphaProof Code.
También queda abierta la viabilidad económica del método. DeepMind realizó el análisis como proyecto de investigación sin cobrar por él, según WIRED, y Google no reveló cuánto costó ni si planea ofrecer un servicio comercial. Las cuatro semanas describen la duración de esta prueba; por sí solas no permiten calcular el costo de aplicar el proceso a otros programas.
