DeepMind logró algo que la industria de la seguridad perseguía desde hace años: usar IA para demostrar matemáticamente que el código de Signal cumple sus promesas de privacidad.
Lo hizo en cuatro semanas y con más de seis millones de líneas de prueba.
El anuncio no es un modelo nuevo ni una función para usuarios. Es AlphaProof Code, un framework de agentes que verifica software con el mismo rigor con el que un matemático demuestra un teorema.
Qué es AlphaProof Code
Los expertos humanos deciden qué propiedades demostrar y escriben las especificaciones. Después, un grupo de agentes de IA, impulsados por Gemini 4 Carbon, genera las pruebas en Lean, un lenguaje que puede verificar cada paso de forma automática.
El kernel de Lean acepta o rechaza la prueba: si pasa, no hay margen para la interpretación.
No es un producto que puedas descargar. Es un framework de investigación con artefactos abiertos, sin API ni precio. Su valor está en demostrar que el método funciona a escala.
Qué se verificó en Signal
El equipo tomó libsignal v0.105.4 y spqr v1.6.0, los compiló para AArch64 y verificó propiedades del handshake PQXDH y del Triple Ratchet: secreto hacia adelante, seguridad después de un compromiso, autenticación y secreto del handshake.
Fueron 6.5 millones de líneas de Lean, 26,000 líneas de especificaciones confiables y cuatro semanas de trabajo de cinco investigadores.
La verificación no encontró vulnerabilidades nuevas en las partes que cubrió. Eso no significa que Signal sea perfecto: significa que, en esas propiedades y en esa compilación, el código hace lo que dice hacer.
La prueba con bugs conocidos
Para comprobar que el sistema detecta errores, el equipo reintrodujo dos bugs ya corregidos de libsignal, conocidos como weak state y small subgroup. AlphaProof Code produjo pruebas de que esas versiones eran inseguras. Es la diferencia entre un auditor que dice “no encontré nada” y uno que puede demostrar que un error específico rompe la seguridad.
Lo que NO prueba
La verificación se hizo sobre una compilación llamada libsignal-cli, no sobre la app que instalas en el teléfono.
No cubre generación de claves, mensajería grupal, sealed sender, protocolos de servidor, canales laterales ni estado multi-dispositivo. Tampoco dice nada sobre WhatsApp, que usa el protocolo Signal pero tiene su propia implementación.
Y no es una bala de plata: las especificaciones las escriben humanos, y si la especificación está mal, la prueba puede ser impecable y aun así demostrar la propiedad equivocada.
Por qué importa
La verificación formal es el estándar más alto de assurance, pero históricamente ha sido carísima: seL4 tomó unas 20 personas-año y CompCert unos seis años. AlphaProof Code muestra que los agentes pueden reducir el trabajo pesado. Eso abre la puerta a firmware médico, redes eléctricas y sistemas críticos.
También deja una pregunta: si la IA escribe las pruebas, ¿quién revisa las especificaciones? DeepMind dice que los humanos revisaron el 100% de las especificaciones y que solo el 1% del código base necesitó una segunda revisión humana.
Es el mismo problema que ya se ve en el código: la IA escribe más rápido, pero los mantenedores revisan más lento.
El siguiente paso es escalar el método y verificar nuevas versiones de libsignal antes de que salgan. Si funciona, la seguridad del software podría dejar de depender de la suerte de una auditoría. ¿Pagarías por una prueba formal de tu software?
Más en: Ciberseguridad, Inteligencia Artificial
