Unos 6,5 millones de líneas de pruebas en Lean, escritas por agentes de IA, demuestran propiedades de seguridad clave del código máquina real de libsignal, la implementación de referencia del protocolo de Signal. Google DeepMind lo presentó el 10 de noviembre de 2026 con el nombre de AlphaProof Code. Lo llamativo no es el tamaño de la prueba, sino lo poco que hay que creerse: unas 26.000 líneas.
Qué se ha demostrado
El equipo compiló el código Rust de libsignal sin modificar, con el rustc estándar, a código máquina AArch64 para Linux, y cargó ese ejecutable en Lean junto con una semántica formal de la arquitectura. Sobre ese binario, los agentes demostraron las propiedades que se esperan de Signal en sus dos piezas centrales, el handshake poscuántico PQXDH y el Triple Ratchet:
| Dato | Valor |
|---|---|
| Pruebas generadas por agentes | ~6,5 millones de líneas de Lean |
| Base que hay que confiar | ~18.000 líneas de especificación + ~8.000 de semántica AArch64 |
| Propiedades | Secreto hacia delante, autenticación, seguridad poscompromiso y secreto del handshake |
| Tiempo | Cuatro semanas |
| Revisión humana de las pruebas | En torno al 1 % del código, señalado por los propios agentes |
Para comprobar que la especificación detecta errores reales, reintrodujeron dos bugs ya corregidos de libsignal en una copia aislada. En los dos casos el sistema produjo una prueba verificada de que el binario resultante incumple los teoremas de seguridad.
Cómo funciona
AlphaProof Code reparte el trabajo como un equipo de investigación. Un agente redactor convierte, con la guía de expertos, modelos y propiedades de la literatura académica en una especificación en Lean; agentes revisores la critican y una persona la aprueba. Después, un equipo de agentes probadores, basados en Gemini Carbon, demuestra que el ejecutable cumple esa especificación. Un agente "portero" solo acepta una prueba si el kernel de Lean la valida y si demuestra exactamente una copia reservada de la especificación, para que ningún agente pueda rebajar lo que se prueba.
Por qué importa
La mayor parte de la verificación formal de protocolos se queda en el diseño. Los análisis previos de Signal estudiaban el handshake y el ratchet por separado y eran anteriores al ratchet poscuántico. Aquí la garantía llega al código que se ejecuta, que es donde suelen esconderse las vulnerabilidades reales: entre lo que dice el diseño y lo que hace la implementación.
El cambio de fondo lo resume el propio artículo: el cuello de botella de la verificación formal ya no es escribir las pruebas, sino la especificación. Una prueba de millones de líneas no hay que leerla, porque si tiene un error lógico Lean la rechaza. Lo que sí hay que revisar es si la especificación dice lo que crees que dice. Para quien construye sistemas críticos, eso desplaza el trabajo experto de demostrar a especificar, y abre la puerta a verificar código que hasta ahora no compensaba por coste: DeepMind menciona firmware de dispositivos médicos y software de redes eléctricas como siguientes candidatos.
Para el resto del sector, también es un argumento comercial. Google presenta la verificación formal como complemento de agentes de defensa como CodeMender frente a amenazas que ya usan IA, y Signal, a través de su CTO Ehren Kret, respalda el método.
Lo que falta por saber
DeepMind publica las especificaciones y las pruebas en Lean, pero no AlphaProof Code como herramienta, ni el coste de cómputo de esas cuatro semanas. La garantía depende además de lo que queda fuera: las primitivas criptográficas se asumen seguras mediante contratos y el resultado cubre el binario para AArch64, no cada compilación de cada plataforma. El propio equipo reconoce que escalarlo a otros sistemas "requiere investigación continuada".
Fuentes
- Introducing AlphaProof Code: a breakthrough in verifying complex software at depth, Google DeepMind, 10 de noviembre de 2026.
- AlphaProof Code: Verifying Signal's Security at the Machine-Code Level, artículo técnico y desarrollo en Lean, Google DeepMind.
- Debate en Hacker News, 10 de noviembre de 2026.