Google DeepMind publica AlphaProof Code: agentes demuestran en Lean la seguridad del código compilado de Signal
Google DeepMind detalló el 10 de noviembre AlphaProof Code, un sistema de agentes que generó alrededor de 6,5 millones de líneas de demostraciones en Lean sobre el código máquina de libsignal, la biblioteca de referencia del protocolo Signal. Las demostraciones cubren el protocolo de enlace poscuántico PQXDH y el Triple Ratchet, con premisas y límites detallados en el artículo técnico.
La demostración se mencionó en una sola línea durante el lanzamiento de Gemini 4 Carbon; ahora está documentada con detalle. Google DeepMind publicó el 10 de noviembre una entrada de blog y un artículo técnico sobre AlphaProof Code, un sistema de agentes que ha demostrado matemáticamente propiedades de seguridad del código de libsignal, la biblioteca de referencia del protocolo Signal. Este protocolo cifra también, con diferentes variantes, WhatsApp, Messenger y Google Messages.
Lo que se ha demostrado
La originalidad radica en el nivel de abstracción de la demostración. La mayoría de las verificaciones de protocolos se limitan a su diseño. En este caso, los investigadores compilaron libsignal con el compilador estándar de Rust para procesadores AArch64 (Arm de 64 bits) en Linux y demostraron que dicho código máquina respeta las propiedades previstas. Estas demostraciones cubren el protocolo de enlace poscuántico PQXDH y el Triple Ratchet: confidencialidad persistente (secreto perfecto hacia adelante), autenticación, seguridad tras el compromiso temporal de un dispositivo y secreto del protocolo de enlace.
Las cifras ilustran la magnitud: unos 6,5 millones de líneas de demostraciones escritas en Lean, un lenguaje de demostración formal cuyo núcleo valida cada paso. Se basan en unas 26 000 líneas de especificaciones y descripciones del procesador que, por su parte, se deben asumir como fiables. El trabajo requirió cuatro semanas a un equipo de cinco personas. El artículo recuerda que la verificación del micronúcleo seL4 exigió veinte años-persona, y la del compilador CompCert, seis.
Cómo trabajan los agentes
AlphaProof Code divide el trabajo al igual que un equipo de investigación. Los humanos deciden qué demostrar y revisan cada especificación, redactada con el apoyo de varios modelos. A continuación, agentes impulsados por Gemini Carbon escriben las demostraciones de forma autónoma. Un agente «guardián» solo acepta una demostración si Lean la valida frente a una copia de la especificación aprobada: por tanto, la fiabilidad del resultado no depende de la de los agentes. Según Google DeepMind, los agentes auditaron después su propio trabajo y solo señalaron en torno al 1% del código de demostración para su revisión humana.
Para comprobar que el sistema distingue entre código seguro y defectuoso, el equipo reintrodujo dos errores reales, ya subsanados, en una copia aislada de libsignal. En ambos casos, el sistema generó una demostración verificada de que la versión con errores no era segura. El director de tecnología de Signal, Ehren Kret, citado en la publicación, lo considera un «avance fundamental». Los artefactos de verificación se han publicado en código abierto.
Los límites, por escrito y con claridad
El artículo técnico es muy explícito respecto a lo que no garantiza. Las demostraciones simbólicas asumen una criptografía perfecta y no dicen nada sobre el secreto computacional de los bytes. Los límites computacionales no resultan válidos frente a un adversario cuántico. La generación de claves no está verificada. La descripción del procesador abarca 467 instrucciones y 31 llamadas al sistema, pero no modela hilos, señales ni enlace dinámico. Por último, el resultado confía en el núcleo de Lean, en las primitivas criptográficas y en los contratos de ciertas rutinas invocadas por el programa.
Nuestro análisis
La verificación formal siempre ha arrastrado un defecto: su coste es prohibitivo para casi todo el software. AlphaProof Code demuestra que los agentes pueden asumir el grueso de las demostraciones, siempre que los humanos determinen qué se debe demostrar y Lean verifique todo lo demás. Se trata de un cambio metodológico más que de una simple proeza aislada: la confianza se desplaza de los agentes, falibles, a un verificador mecánico. No obstante, el resultado se circunscribe a un perímetro muy acotado, un pequeño programa de prueba por línea de comandos, una arquitectura concreta y premisas criptográficas asumidas. La primicia que reivindican y el coste computacional real aún deben ser evaluados por otros equipos, más aún cuando Google DeepMind no aclara si pondrá la herramienta a disposición de terceros. Para las empresas de software crítico, el dilema ya es práctico: ¿quién se encargará de redactar y revisar las especificaciones, ahora la principal labor humana?
Fuentes
- Google DeepMind — Introducing AlphaProof Code: a breakthrough in verifying complex software at depth (10 de noviembre de 2026) Fuente primaria
- Google DeepMind — AlphaProof Code: Verifying Signal's Security at the Machine-Code Level (artículo técnico y desarrollo en Lean) Fuente primaria
- The Register — Google DeepMind melds humans and AI agents to vet Signal's secure messaging techniques Fuente secundaria
Una fuente primaria procede directamente de la empresa, el laboratorio o la organización implicados. Una fuente secundaria recoge la información sin ser su autora: la señalamos como tal. ¿Has visto un error? Consulta nuestra política de correcciones.
