Principales destacados
- Criptografía bajo verificación: AlphaProof Code demostró matemáticamente importantes garantías del protocolo de seguridad de Signal.
- Pruebas de vulnerabilidades: la herramienta identificó fallos conocidos en versiones antiguas del protocolo, pero no encontró nuevas vulnerabilidades en las partes analizadas.
- Impacto más allá de Signal: esta tecnología también tiene implicaciones para la seguridad de servicios como WhatsApp y Google Messages, que utilizan el protocolo Signal.
La inteligencia artificial está comenzando a asumir una tarea que, hasta hace poco, requería un trabajo matemático extremadamente especializado: demostrar que los sistemas de software realmente cumplen sus promesas de seguridad.
Investigadores de Google DeepMind utilizaron una nueva estructura de inteligencia artificial, llamada AlphaProof Code, para verificar matemáticamente algunas de las principales garantías criptográficas del protocolo Signal. El experimento, realizado durante cuatro semanas, representa un avance en la aplicación de la IA a la verificación formal de software.
Según un reportaje de WIRED publicado el 10 de noviembre, el trabajo no identificó nuevas vulnerabilidades en las partes analizadas del protocolo.
Y esto merece atención. Al fin y al cabo, estamos hablando de una tecnología que protege las conversaciones de miles de millones de personas.
🔐 No se trata solamente de proteger los mensajes de Signal
El protocolo Signal es conocido por implementar el cifrado de extremo a extremo, un mecanismo que impide que terceros lean el contenido de las conversaciones durante su transmisión.
Pero su influencia va mucho más allá de la aplicación que lleva su nombre.
Otros servicios populares también utilizan tecnologías derivadas de este protocolo, entre ellos WhatsApp y Google Messages.
Qué cambia con esta investigación: en lugar de depender exclusivamente de pruebas convencionales y auditorías de seguridad, los investigadores utilizaron IA para construir demostraciones matemáticas de que determinadas propiedades criptográficas se cumplen.
La llamada verificación formal es un enfoque especialmente importante para los sistemas críticos. Permite demostrar, mediante métodos matemáticos, que un programa cumple determinadas especificaciones.
El problema es que este proceso suele ser lento, complejo y costoso.
Y es precisamente ahí donde la inteligencia artificial puede marcar la diferencia.
🧪 La IA también tuvo que enfrentarse a fallos conocidos
Antes de analizar las garantías de seguridad, los investigadores pusieron AlphaProof Code a prueba con versiones antiguas de Signal que presentaban vulnerabilidades ya conocidas.
El resultado fue importante: la herramienta consiguió identificar correctamente esos fallos y demostrar que las versiones comprometidas no podían superar la verificación formal.
Esta prueba ayudó a evaluar si el sistema realmente podía distinguir entre implementaciones seguras y aquellas que presentaban problemas.
Un detalle importante: la investigación no representa una auditoría completa de la aplicación Signal. El trabajo se concentró en propiedades específicas del protocolo y no verificó todo el código de las aplicaciones móviles.
Por lo tanto, no significa que Google haya certificado la seguridad absoluta de Signal, WhatsApp o Google Messages.
🤝 Signal también ve ventajas en este enfoque
El trabajo de DeepMind aprovechó investigaciones anteriores de verificación formal realizadas por el propio Signal.
Según Ehren Kret, director de tecnología de la organización, el nuevo enfoque permite ampliar significativamente el alcance de verificaciones que antes se concentraban en partes más pequeñas del código.
El ejecutivo también afirmó que el resultado ofrece todavía más confianza ante el crecimiento de las amenazas de seguridad impulsadas por inteligencia artificial.
💡 La cuestión no es solamente encontrar vulnerabilidades. También es poder demostrar matemáticamente que determinadas garantías de seguridad realmente se cumplen.
DeepMind pretende publicar la especificación y las demostraciones desarrolladas durante el proyecto, lo que permitirá que otros investigadores aprovechen este material en iniciativas similares.
🏁 Una carrera por la verificación automatizada de software
Google no está solo en este intento de acercar la inteligencia artificial a las demostraciones matemáticas.
En abril de 2026, Signal, Beneficial AI Foundation y Lean FRO lanzaron Signal Shot, una iniciativa pública para verificar el protocolo Signal y su implementación en Rust utilizando el asistente de demostraciones Lean.
El objetivo es traducir el código real de Signal a Lean y demostrar que su implementación corresponde a un modelo matemático previamente verificado.
Aunque comparten objetivos similares, el trabajo de DeepMind es independiente de esta iniciativa.
La diferencia está en la velocidad y la escala que puede proporcionar la IA. Si los agentes inteligentes consiguen producir, revisar y corregir demostraciones matemáticas bajo supervisión humana, tareas que antes requerían largos períodos de trabajo especializado podrían volverse más accesibles.
💰 Pero ¿cuánto cuesta verificar todo esto?
Existe una cuestión que todavía necesita respuesta: la viabilidad económica.
DeepMind realizó el experimento gratuitamente como parte de una iniciativa de investigación. Google no reveló cuánto costó el proyecto ni confirmó si pretende convertir esta tecnología en un producto comercial.
Swarat Chaudhuri, científico investigador de DeepMind, destacó que uno de los avances importantes fue permitir que los agentes de IA contribuyeran al desarrollo de las demostraciones y corrigieran sus propios resultados, mientras los especialistas humanos realizaban revisiones en etapas fundamentales.
También hizo una advertencia importante sobre los límites de la automatización:
No queremos un mundo en el que la IA genere los objetivos, produzca las demostraciones y después aplique pruebas escritas por ella misma.
La preocupación tiene sentido. En seguridad digital, permitir que un sistema produzca sus propias reglas y valide por sí solo los resultados podría crear una falsa sensación de confianza.
🔎 El próximo desafío es verificar mucho más que mensajes
El experimento con Signal apunta a una posibilidad mayor: utilizar agentes de inteligencia artificial para verificar matemáticamente sistemas operativos, software financiero, infraestructura digital y otros componentes críticos.
Pero todavía queda un largo camino para llegar a ese escenario.
La propia DeepMind reconoce que ampliar este enfoque a prácticamente todo el software existente será un desafío considerable.
Por ahora, el resultado ofrece una demostración concreta de cómo los agentes de IA pueden ayudar a los especialistas a enfrentar uno de los problemas más antiguos de la ingeniería de software: demostrar que un programa hace exactamente lo que debería hacer.
Y cuando se trata de criptografía, demostrar la seguridad puede ser tan importante como encontrar una vulnerabilidad.
