El código de AlphaProof demostró que la criptografía de Signal es correcta — al nivel del binario compilado

Seis millones y medio de líneas de Lean, producidas en cuatro semanas, por equipos de agentes en cuya escritura no participó ningún humano. Esa es la cifra principal que Google DeepMind publicó el 10 de noviembre de 2026 para AlphaProof Code, un marco agéntico para la verificación formal que el laboratorio usó para verificar mecánicamente el núcleo criptográfico del protocolo Signal —y, de forma inusual, para comprobarlo a nivel del binario AArch64 compilado en lugar del documento de diseño situado por encima. Los modelos que hicieron el trabajo son otra cuestión. una clave de API al precio de lista del proveedor con 0% de recargo El motor de los agentes de prueba no es algo que ofrezcamos.

El framework no es un modelo al que puedas llamar. Es un arnés: expertos humanos deciden qué debe ser cierto, una combinación de modelos convierte esos objetivos en especificaciones de Lean, y luego equipos de agentes que escriben demostraciones —el blog nombra a Gemini Carbon como el motor— completan las demostraciones hasta que el kernel de Lean las acepta. Lo que se lanzó junto con el anuncio es el conjunto de artefactos, en github.com/google-deepmind/code-verification, y un artículo técnico que es mucho más franco sobre los límites del resultado de lo que lo es la entrada del blog. La mayor parte de lo que sigue procede de ese artículo, porque es en el artículo donde están los números interesantes.

¿Qué se demostró realmente y contra qué?

El objetivo es libsignal v0.105.4 con spqr v1.6.0, compilado con el rustc 1.98.1 estándar, enlazado estáticamente contra musl y emitido como un único ejecutable de Linux para AArch64. Ese detalle importa más que cualquier benchmark: las pruebas versan sobre los bytes que se ejecutarían en un teléfono, no sobre una función de Rust cuya traducción fiel se confía al compilador. El equipo verificó aproximadamente 560 KB de código fuente de libsignal, alrededor de 140.000 instrucciones AArch64, y lo hizo escribiendo un modelo Lean del conjunto de instrucciones —467 instrucciones y 31 llamadas al sistema, en 7.578 líneas— y demostrando después que la imagen ELF real, cargada y ejecutada bajo ese modelo, preserva las propiedades de seguridad.

Las propiedades son las que pediría un ingeniero de protocolos. Diez teoremas simbólicos cubren el secreto hacia adelante, la seguridad tras el compromiso, el secreto del iniciador y del respondedor, la autenticación, y cinco corolarios del teorema 1 de PQXDH. El resultado principal se denomina signal_session_secure_placed. También hay una vía computacional con una cota concreta, y las dos vías usan modelos de adversario distintos: el lado simbólico (Dolev–Yao, mediante el marco DyLean) incluso cubre a un atacante cuántico que rompe Diffie–Hellman después del handshake, mientras que el lado computacional solo cubre adversarios clásicos.

Adónde van los seis millones de líneas

«Más de seis millones de líneas» es la expresión del blog, y es exacta pero tosca. El desglose del artículo es el útil, y merece la pena leerlo como una tabla de costes en lugar de como un alarde:

• Pruebas para el binario — 5,3 millones de líneas, la mayor parte del trabajo, que cubren la semántica del código máquina y el refinamiento desde el modelo simbólico hasta el ejecutable.

Pruebas computacionales — unas 860.000 líneas.

• Pruebas simbólicas — unas 350.000 líneas.

• Pruebas de refutación de errores — unas 140.000 líneas, para las dos vulnerabilidades reintroducidas deliberadamente que se describen a continuación.

Pruebas del asignador — aproximadamente 70.000 líneas.

Casi siete millones de líneas si se cuentan los comentarios y las líneas en blanco, cosa que el artículo hace y el blog no. En cualquier caso, la proporción que importa es la que hay entre la prueba y lo probado: 6,5 millones de líneas de Lean para establecer propiedades de un binario de 560 KB. Esa proporción es la medida honesta de lo lejos que está esta técnica de ser rutinaria, y es la cifra que hay que citar cuando alguien pregunta si la verificación formal se ha vuelto barata.

La base de confianza es más pequeña que la prueba, y esa es la cuestión.

Una prueba vale solo tanto como aquello que asume. El artículo es específico al respecto, y esa especificidad es lo que lo distingue de una nota de prensa. Las especificaciones de confianza ocupan unas 18.000 líneas (28.000 con documentación), la semántica de AArch64 unas 8.000 y la codificación en Lean del código máquina alrededor de 95.000. Treinta y siete rutinas se sustituyen por contratos en lugar de verificarse: la compresión SHA-256 y SHA-512, AES-256-CBC, X25519, las operaciones de curvas de Edwards, Kyber1024 y ML-KEM-768, y HMAC de libcrux. Dieciocho puntos de entrada de pánico se asumen asimismo en lugar de demostrarse.

Así que la afirmación no es «todo está demostrado». La afirmación es que la lógica del protocolo criptográfico, la máquina de estados de la sesión y el refinamiento desde esa lógica hasta las instrucciones realmente ejecutadas están demostrados, mientras que las primitivas subyacentes se confían tal como todo proyecto de verificación confía en sus primitivas. El compilador de Rust, en particular, no forma parte de la base de confianza: el equipo evitó tener que confiar en él razonando a nivel de código máquina, que es el mismo truco que les permite sortear por completo un compilador verificado. Como contexto sobre la escala, el artículo cita seL4 con aproximadamente 20 años-persona y CompCert con unos 6.

Dos errores, reintroducidos a propósito

Un sistema de verificación que siempre dice «correcto» es imposible de poner a prueba. Así que el equipo tomó dos vulnerabilidades que se habían encontrado y corregido previamente en el código de Signal —un error de estado débil y un error de subgrupo pequeño—, las reintrodujo en una copia aislada y volvió a ejecutar el pipeline. En ambos casos, AlphaProof Code produjo una prueba verificada por máquina de que la versión con errores no cumple el teorema de seguridad: la declaración simbólica se reduce a ¬Sec(Asm_bug).

El artículo añade una salvedad que una página de marketing habría omitido: refutar el computacional teorema para esos fallos es «mucho más difícil» y se dejó abierto. En otras palabras, la prueba negativa funciona limpiamente en la vía simbólica y todavía no funciona en la computacional. Ese es exactamente el tipo de asimetría que un lector debería conocer antes de tratar el marco como un detector de fallos.

Cómo se ejecutaron los agentes

Cinco investigadores durante cuatro semanas, cada uno ejecutando agentes sin cesar. La escritura de las demostraciones propiamente dicha la realizaron equipos de 40 a 80 agentes, que se ejecutaron entre 24 y 72 horas en una sola máquina por equipo, con un agente supervisor por encima del orquestador del equipo. Un agente guardián comprueba cada envío con comparador contra una copia reservada de la especificación y contra el kernel de Lean —una defensa contra que un agente demuestre una versión sutilmente debilitada de lo que se pidió.

El trabajo humano se concentró al principio en las especificaciones. Un experto revisó cada especificación antes de que comenzara el trabajo de demostración, y la propia pasada de auditoría de los agentes señaló aproximadamente el 1 % de la base de código para atención humana. Ningún humano escribió código de demostración. El artículo también es directo sobre la ingeniería: una compilación limpia puede tardar varias horas; al principio, una edición menor del código fuente o un binario recompilado obligaban a realizar reparaciones extensas en las demostraciones; y hay «amplio margen de optimización» tanto en las demostraciones generadas por IA como en las propias técnicas de demostración.

Lo que las pruebas no cubren

Las limitaciones son lo suficientemente extensas como para constituir la sección más importante del artículo, y se exponen con claridad. No se establece ninguna garantía poscuántica para la propiedad de recuperación de SPQR — los teoremas del trinquete suponen que el atacante elige las claves de SPQR. No se demuestra la privacidad de la carga útil. No se demuestra la autenticación del respondedor para el primer mensaje de un handshake que nunca se promueve. El modelo permite una sesión por promoción, longitudes de mensaje fijas, ningún estado multidispositivo y claves de identidad de confianza en el primer uso.

También hay una cota que se vuelve vacua. El término de falsificación de MAC de 8 bytes es al menos 2⁻⁶⁴ por intento y crece cuadráticamente en mensajes y épocas, lo que significa que la cota deja de decir nada para una sola sesión de aproximadamente 25.000 mensajes, o para 2²⁰ sesiones de 2¹⁰ mensajes. Y el objeto de la prueba es la compilación del equipo de libsignal-cli ejecutándose como un proceso nuevo —no la aplicación Signal de tu teléfono. Varias suposiciones del entorno se argumentan de manera informal en lugar de demostrarse.

No hay API, ni precio, ni modelo al que llamar.

Esta es la parte que decepcionará a cualquiera que llegue desde una tabla de clasificación de modelos. AlphaProof Code es un marco de investigación y un conjunto de artefactos publicados. No hay endpoint, ni tarifa por token, ni lista de espera, ni pesos: el repositorio contiene el desarrollo en Lean, la semántica de AArch64, el binding de libsignal y las especificaciones, no un checkpoint. El blog dice que los artefactos son de código abierto; la página de inicio no indica ninguna licencia, lo cual vale la pena comprobar antes de que alguien planee construir sobre ello.

Los modelos que hicieron el trabajo son otra cuestión. El artículo nombra G​emini 4 Carbon para los agentes de demostración y afirma que Claude Opus 5.5 se utilizó junto con otros modelos para redactar y revisar especificaciones. Claude Opus 5.5 está hoy en el catálogo de OrcaRouter a $4 por millón de tokens de entrada y $20 por millón de salida, con el precio de lista del proveedor trasladado sin margen (0 %); así que, si la conclusión práctica que buscas es «ejecutar un bucle de redacción de especificaciones con el modelo que usó el artículo», esa parte es una llamada normal a la API, y un cambio de precio del proveedor se refleja de nuestro lado el mismo día. El motor de los agentes de demostración no es algo que ofrezcamos, y nada de lo aquí dicho implica que alojemos AlphaProof Code en sí.

Por qué esto es más importante que el resultado de Signal

La verificación de Signal es impresionante por sí misma: la primera verificación formal de la implementación de un protocolo ampliamente desplegado por cualquier método, con o sin IA, según DeepMind, y la primera vez que la IA ha verificado un protocolo criptográfico desplegado con este nivel de profundidad. Pero la afirmación transferible es el flujo de trabajo. Un equipo de cinco personas, en cuatro semanas, con un paso de revisión de especificaciones y un agente guardián, produjo un corpus de demostraciones que antes habría sido un proyecto de varios años. Si esa proporción se mantiene aunque sea de forma aproximada, cambia el conjunto de sistemas que pueden permitirse la verificación: firmware de dispositivos médicos, software de redes eléctricas, ese tipo de código que actualmente recibe una revisión de código y una plegaria.

No se ha probado si se sostiene. La criptografía de Signal está especificada de forma inusualmente rigurosa, el equipo hizo que los propios ingenieros de Signal revisaran la metodología, y las primitivas se subcontrataron en vez de verificarse. El próximo sistema no será tan complaciente. El propio planteamiento del artículo —combinar la verificación formal con agentes automatizados de defensa como CodeMender— es la forma honesta de la propuesta: la verificación te dice qué es cierto, y otra cosa tiene que arreglar lo que no lo es.

Qué ver

Tres cosas llevarían esto de ser un artículo histórico a una técnica industrial. Una segunda base de código independiente verificada por alguien ajeno a Google, idealmente una en la que la especificación tuviera que escribirse desde cero en lugar de adaptarse a partir de un análisis existente. Una cifra de coste —horas de agente, horas de acelerador, dólares— porque cuatro semanas y equipos de 40 a 80 agentes no es una unidad con la que ningún responsable de ingeniería pueda presupuestar. Y la refutación de errores de la vía computacional, que el artículo deja abierta y que marca la diferencia entre un sistema que demuestra propiedades y un sistema que también puede decirte, computacionalmente, que un binario específico está roto.

Hasta entonces, lee el repositorio de artefactos en lugar del anuncio. Las pruebas están allí, Lean las verifica, y el artículo te dice exactamente qué asumen.