En un ensayo técnico, investigadores de Google DeepMind aplicaron una inteligencia artificial para realizar verificaciones formales sobre determinadas garantías del protocolo criptográfico que protege los mensajes de Signal. Según Wired, el proyecto se desarrolló durante cuatro semanas y no encontró fallas nuevas en las partes analizadas.

El estudio utilizó un sistema desarrollado por la propia compañía denominado AlphaProof Code, descrito por los autores como una prueba de concepto: una demostración inicial de que la idea funciona antes de escalarla.

La verificación formal consiste en plantear en lenguaje matemático lo que debe cumplir un programa y demostrar que efectivamente se cumple. Para quienes trabajan en seguridad informática, es una meta largamente perseguida, y la IA aparece como una herramienta que puede acortar principalmente la fase de construcción de la prueba.

El análisis cubrió solo ciertas garantías del protocolo y de su implementación en la app móvil de Signal, no la totalidad de la plataforma. Además, se probó la herramienta con versiones antiguas de Signal que ya tenían fallas conocidas y corregidas; el sistema las detectó y mostró que esas versiones no podían verificarse.

DeepMind adelantó que publicará la especificación y la demostración desarrolladas para que otros equipos las utilicen en trabajos similares. Los investigadores reconocen que parten con cierta ventaja, porque la Signal Foundation ya había obtenido verificaciones formales sobre porciones más reducidas del código.

Este antecedente forma parte de un proyecto público llamado Signal Shot, iniciado el 20 de abril de 2026 por la Beneficial AI Foundation, Signal y Lean FRO, según el sitio del proyecto. Su objetivo es verificar tanto el protocolo como la versión completa de la aplicación con el asistente de demostraciones Lean.

El protocolo de Signal sirve como base para el cifrado de WhatsApp y Google Messages, por lo que, según Wired, los resultados del piloto funcionan como una validación independiente de la criptografía que protege una enorme cantidad de comunicaciones.

Ehren Kret, director de tecnología de Signal, afirmó que el enfoque de DeepMind amplía significativamente lo logrado anteriormente, que se centraba en componentes aislados. Indicó que la verificación de la implementación ofrece mayor confianza en las garantías de privacidad ante escenarios de ciberseguridad potenciados por IA.

Swarat Chaudhuri, investigador de DeepMind, fue prudente respecto al alcance: “falta mucho para escalar esto a todo el software del mundo, y queremos hacerlo”. Explicó que el método combina agentes automatizados y revisión humana en momentos clave y que no buscan un esquema en el que la IA genere metas y pruebas sin control.

Pushmeet Kohli, científico jefe de Google Cloud, comentó que estos avances ayudan a entender cómo aplicar enfoques de verificación a proyectos de seguridad a gran escala, sin ampliar detalles específicos.