DeepMind demostró matemáticamente la seguridad del código de Signal en 4 semanas en lugar de años

Cualquiera que haya escrito criptografía conoce una verdad incómoda: un protocolo puede demostrarse de forma elegante sobre el papel y, aun así, la vulnerabilidad acabará estando en el código. Entre el esquema y la implementación hay un abismo, y ahí es donde viven los errores de verdad. Google DeepMind afirma haber enseñado a agentes de IA a cerrar ese abismo para uno de los protocolos más importantes del mundo, el que protege las conversaciones en Signal y Google Messages.

Qué se hizo exactamente

El sistema se llama AlphaProof Code. Es un framework multiagente basado en varios LLM que reparte el trabajo igual que lo haría un equipo de investigación. Primero, expertos humanos junto con modelos traducen los objetivos de seguridad de Signal a especificaciones matemáticas formales. Cada especificación la revisa manualmente una persona. Después, los agentes basados en Gemini Carbon escriben las propias demostraciones en el lenguaje Lean, con un resultado de más de seis millones de líneas.

Lo siguiente es lo más práctico. Lean mismo comprueba la corrección de cada demostración, de modo que no hace falta confiar ciegamente en el modelo: una conclusión errónea simplemente no superará la verificación. Además, los agentes auditaron el resultado y señalaron los puntos que requieren la mirada de una persona. Es aproximadamente el 1 % de la base de código. Los expertos se concentraron en esos puntos en lugar de releer millones de líneas.

Por qué no es una auditoría más

La verificación formal habitual de protocolos se detiene en el nivel del diseño: se demuestra que el esquema es seguro. Aquí los agentes fueron más lejos y demostraron propiedades del código compilado que se ejecuta en los dispositivos. Por ejemplo, que los mensajes siguen protegidos antes y después de un compromiso temporal de un dispositivo.

Para comprobar la honestidad del sistema, los autores realizaron una prueba sencilla. En una versión aislada del código de Signal reintrodujeron dos errores reales que ya habían sido corregidos. En ambos casos, el sistema generó una demostración verificable por máquina de que esa versión es insegura. Es decir, la herramienta distingue el código correcto del incorrecto, y no se limita a «aprobar» todo.

Según DeepMind, todo el trabajo llevó cuatro semanas, mientras que a los equipos de expertos tradicionalmente les ha llevado años. El director técnico de Signal, Eren Kret, calificó la traducción automática de código de producción a teoremas de Lean como un avance importante.

Limitaciones y conclusiones prácticas

Conviene mirar la escala con sobriedad. Es un único protocolo, estudiado durante mucho tiempo y con minuciosidad, y la mayor parte de las cifras declaradas se basa en el autoinforme de DeepMind. Los humanos no han desaparecido del proceso: lo que se considera «seguro» lo siguen definiendo los expertos, y un error en la especificación produce la demostración de algo que no era lo que se buscaba. Los propios autores dicen que para escalar hacen falta más investigaciones. Las áreas anunciadas, el firmware de dispositivos médicos y el software para redes eléctricas, por ahora son solo planes.

¿Qué significa esto para desarrolladores y fundadores?

• El esquema «el LLM escribe, el verificador formal acepta o rechaza» funciona para tareas en las que el coste del error es alto. Al modelo se le permite equivocarse; al verificador, no.
• Si desarrollas criptografía, lógica de pagos o código embebido crítico, la verificación formal deja de ser patrimonio de equipos académicos con presupuestos de varios años.
• La habilidad de formular especificaciones se vuelve más valiosa que la de escribir demostraciones. El cuello de botella se desplaza a la pregunta «¿qué queremos garantizar exactamente?».

Un punto a favor adicional es que DeepMind abre los artefactos de verificación. Se pueden estudiar y usar como modelo para experimentos propios con Lean y agentes. Junto con herramientas como CodeMender, que encuentran y corrigen vulnerabilidades, las demostraciones formales pasan a ser parte del perímetro defensivo habitual y no una rareza académica.