Google DeepMind utiliza agentes de IA para verificar el código máquina central de Signal

Google DeepMind presentó AlphaProof Code el 10 de noviembre de 2026, utilizando equipos de agentes de IA para generar pruebas Lean verificadas por máquina de propiedades de seguridad especificadas en el código compilado de libsignal de Signal. El equipo de investigación, formado por cinco personas, completó las pruebas en cuatro semanas y publicó sus especificaciones y artefactos de verificación para que expertos externos pudieran revisarlos.

El trabajo fue más allá de un modelo abstracto del diseño del protocolo de Signal y llegó hasta su implementación compilada. Los investigadores envolvieron los crates sin modificar libsignal v0.105.4 y SPQR v1.6.0 en un pequeño programa de línea de comandos y luego utilizaron rustc estándar para crear un ejecutable AArch64 para Linux enlazado estáticamente. El artículo técnico describe el resultado como las primeras pruebas de seguridad a nivel de protocolo del código sin modificar de una implementación de protocolo criptográfico ampliamente desplegada.

Cómo AlphaProof Code repartió el trabajo

Cinco investigadores dedicaron cuatro semanas a las pruebas y ejecutaron agentes continuamente en sus estaciones de trabajo mientras desarrollaban en paralelo pruebas simbólicas y computacionales. Según el artículo, los agentes generaron unos 6,5 millones de líneas de código de prueba Lean verificado por máquina, sustentadas en aproximadamente 26.000 líneas de especificaciones confiables y semántica de AArch64.

Los seres humanos seleccionaron las propiedades, resolvieron ambigüedades y disyuntivas de seguridad, revisaron las especificaciones y conservaron la aprobación final. Agentes impulsados por Gemini 4 Carbon y Claude Opus 5.5 redactaron y revisaron esas especificaciones; la revisión también incluyó un modelo de otra familia. Después, equipos de agentes de Gemini 4 Carbon generaron todo el código de prueba; ninguno de los autores escribió código de prueba. En las campañas habituales se utilizaron entre 40 y 80 agentes en una sola máquina durante períodos de entre 24 y 72 horas. Un orquestador y los líderes de equipo coordinaban a los agentes encargados de las pruebas, mientras que los responsables de arquitectura e integración mantenían la base de pruebas compartida.

Un mecanismo de control solo aceptaba una prueba después de que el núcleo de Lean la verificara y un comparador confirmara que coincidía con la especificación reservada y aprobada por personas, incluidas todas las definiciones transitivas, y que solo utilizaba los axiomas estándar de Lean. Los agentes podían proponer pequeñas modificaciones cuando las pruebas revelaban problemas en las especificaciones, pero cualquier cambio en los supuestos de confianza requería la aprobación de una persona o una política definida por el usuario, y se registraba con su justificación. Este control aborda un riesgo documentado de las pruebas generadas por agentes: una especificación puede debilitarse indirectamente a través de una de sus definiciones.

Cobertura de seguridad y pruebas con errores históricos

El objetivo de la verificación era el código de sesiones uno a uno, que abarca el protocolo de enlace PQXDH y la mensajería Triple Ratchet. Los investigadores informan de dos demostraciones independientes: diez teoremas simbólicos bajo supuestos criptográficos idealizados y una prueba computacional que acota la ventaja de un atacante mediante supuestos criptográficos y términos estadísticos. Entre las propiedades se incluyen el secreto hacia adelante, que protege los mensajes anteriores si se sustrae el estado actual; la autenticación; la seguridad posterior al compromiso, que se refiere a la recuperación tras un compromiso; y el secreto del protocolo de enlace. Además, el argumento simbólico contempla la preservación del secreto del protocolo de enlace tras una futura vulneración de Diffie–Hellman.

Para comprobar si esas especificaciones podían detectar errores reales, el equipo revirtió las correcciones de dos errores de libsignal que ya se habían reparado, conocidos como estado débil y subgrupo pequeño, y volvió a compilar los binarios modificados. En ambos casos, generó pruebas Lean que demostraban que el teorema simbólico de seguridad no se cumplía. El repositorio público de verificación organiza por separado el material computacional, simbólico, de binarios compartidos y de semántica de AArch64, y explica cómo volver a compilar y verificar las pruebas de forma independiente.

Ehren Kret, director de tecnología de Signal, afirmó que el trabajo «nos da aún más confianza en las garantías de privacidad de nuestro código».

Límites y próximos pasos

Las garantías están muy lejos de certificar las aplicaciones completas de Signal. Se refieren a la compilación de libsignal-cli de los investigadores, ejecutada como un proceso nuevo; la generación de claves no se verificó, la mensajería grupal quedó para trabajos futuros y el escenario no contempla canales laterales ni estados multidispositivo. Los contratos de confianza representan las primitivas criptográficas de bajo nivel y determinadas rutinas de salida y de biblioteca. Por tanto, el resultado también depende de esos contratos, de las especificaciones aprobadas, del núcleo de Lean, de la semántica de AArch64 y de los supuestos sobre las primitivas.

El artículo afirma que ninguno de los dos argumentos demuestra la recuperación poscuántica que SPQR está diseñado para aportar: el teorema computacional abarca a atacantes clásicos, mientras que los teoremas simbólicos del ratchet permiten que el atacante elija las claves de SPQR. El modelo computacional también limita varias acciones del atacante y se vuelve vacuo cuando la cantidad de mensajes y sesiones alcanza una escala suficientemente grande. Estos límites definen qué aspectos debe aceptar como confiables una persona que revise el trabajo desde fuera antes de considerar las pruebas verificadas por máquina una garantía de seguridad para una implementación concreta.

Los próximos pasos que plantean los investigadores son reforzar los teoremas, reducir la base de confianza verificando más rutinas conectadas y vinculando los contratos criptográficos con implementaciones verificadas, y ampliar la cobertura a la mensajería grupal, el remitente sellado y los protocolos del servidor. Su objetivo de verificar las nuevas versiones de libsignal antes de su distribución es una meta de investigación, no un despliegue anunciado.

La importancia inmediata del resultado radica en la división del trabajo que pone de manifiesto: los agentes se encargaron de construir las demostraciones, mientras que la garantía sigue dependiendo de especificaciones revisadas por personas y de supuestos explícitos. La publicación de las demostraciones y los procedimientos de comprobación permite a revisores externos poner a prueba esos fundamentos, mientras los investigadores trabajan para incorporar este flujo de trabajo al desarrollo continuo de libsignal.