DeepMind demostró formalmente con IA las garantías clave de Signal en 4 semanas

Las pruebas demuestran que el código funciona en los casos que a usted se le ocurrió comprobar. La verificación formal responde a otra pregunta: ¿se puede demostrar matemáticamente que el código no violará una propiedad dada con ningún dato de entrada? En seguridad es un viejo sueño, pero en la práctica choca con el coste. Ahora tiene un argumento notable a su favor: Google DeepMind demostró con agentes de IA las garantías clave del protocolo criptográfico de Signal.

Qué se hizo exactamente

El equipo de DeepMind usó un nuevo marco llamado AlphaProof Code. El trabajo duró cuatro semanas y se planteó como prueba de concepto. El protocolo Signal protege las conversaciones no solo en la propia aplicación de mensajería, sino también en Google Messages y WhatsApp, de modo que es uno de los protocolos criptográficos más utilizados del mundo.

En pocas palabras, la verificación consta de tres pasos. Primero, las personas describen qué propiedades debe tener el código. Después, esa descripción se traduce a fórmulas. Por último, se construye una demostración de que el código se ajusta a esas fórmulas. Antes de la era de la IA, los tres pasos consumían meses de trabajo de especialistas. Según los investigadores, la IA agéntica reduce drásticamente el último paso, el más laborioso.

El sistema no encontró nuevas vulnerabilidades en las partes verificadas del protocolo. Pero también se probó lo contrario: en versiones antiguas de Signal con errores corregidos hace tiempo, AlphaProof Code mostró correctamente que no era posible construir la demostración. Para los profesionales es una señal importante. La herramienta no sella un «todo es seguro», sino que de verdad tropieza con defectos reales.

Dónde está la trampa

Conviene evaluar la escala con sobriedad. El análisis no abarcó toda la aplicación móvil de Signal, solo partes concretas del protocolo. Además, DeepMind no partió de cero: Signal Foundation ya había realizado antes la verificación formal de fragmentos de código más pequeños. Eso dio al equipo ventaja. El director técnico de Signal, Eren Kret, señala que el enfoque de DeepMind permite ampliar de forma significativa la cobertura.

La pregunta principal de la industria es la escala y el coste. DeepMind realizó el análisis gratis, como proyecto de investigación, y en Google se negaron a decir cuánto costó. Tampoco respondieron si la compañía planea un producto o servicio comercial de verificación formal. El propio investigador Swarat Chaudhuri admite que «aún queda un largo camino» para escalarlo a todo el software del mundo.

El humano sigue en el circuito

Lo más interesante es el proceso que el equipo llama «human-AI collaboration». Los agentes contribuyen en casi todas las etapas y corrigen sus propios errores, pero en los puntos clave de decisión piden revisión humana. Chaudhuri dice sin rodeos que no quiere un «mundo de vibra» en el que la IA formule por sí sola los objetivos, escriba por sí sola las demostraciones y, en esencia, se entregue a sí misma los exámenes. Hace falta un punto medio.

La lógica es clara. Si un modelo decide qué hay que demostrar y además lo demuestra, un error en la formulación del objetivo pasará inadvertido. La demostración será formalmente correcta, pero verificará lo que no toca. Por eso la especificación de propiedades debe aprobarla un humano con criterio.

Qué hacer con esto

Los desarrolladores y fundadores cuyo producto depende de lógica crítica (pagos, criptografía, protocolos de sincronización) deberían empezar a considerar la verificación formal como una opción real, y no como una rareza académica. Mientras se desconozca su coste, es pronto para incluirla en el presupuesto. Pero hay un beneficio concreto: DeepMind publica la especificación y la demostración de Signal, que pueden estudiarse y utilizarse en otros trabajos de verificación.

Según Pushmeet Kohli, de Google Cloud y DeepMind, los bancos y otras empresas que dependen de garantías de corrección podrán decir: «puedo demostrar estas propiedades». Por ahora es más una promesa que un producto terminado. Pero la verificación con IA ha superado su primera prueba seria, con un protocolo real y de uso masivo.