La mayoría de las noticias de seguridad sobre IA tratan de encontrar fallos. AlphaProof Code, de Google DeepMind, trata de demostrar su ausencia, al menos para propiedades concretas, en un código que usan miles de millones de personas. DeepMind dice que sus agentes demostraron propiedades de seguridad clave del código compilado del protocolo de Signal, que también sustenta el cifrado de WhatsApp, Messenger y Google Messages. Lo presenta como la primera vez que la implementación de un protocolo así se verifica formalmente por cualquier método.
El método de trabajo importa tanto como el resultado. Un agente redactor de especificaciones trabajó con los investigadores para convertir en Lean los objetivos de seguridad de la literatura, agentes revisores criticaron los borradores y personas aprobaron cada especificación. Después, agentes demostradores con Gemini 4 Carbon escribieron las demostraciones. Marcaron alrededor del uno por ciento del código para una segunda revisión humana, y el núcleo de Lean comprobó todo lo demás. Según el artículo que acompaña al anuncio, un equipo de cinco personas hizo el trabajo en cuatro semanas, cada una con agentes funcionando sin parar en su propio ordenador, sobre la versión 0.105.4 de libsignal.
La prueba que debería convencer a los escépticos es la de los fallos. El equipo reintrodujo dos fallos reales, ya corregidos, en una copia aislada del código. En ambos casos el sistema produjo una demostración verificada por máquina de que la versión con el fallo era insegura. Uno consistía en que libsignal guardaba el estado de una sesión nueva, incluida una clave secreta, tras un mensaje que solo debía descifrarse con una sesión anterior. El director de tecnología de Signal, Ehren Kret, dijo que las verificaciones previas cubrían partes más pequeñas del código y que traducir código en producción a teoremas válidos de Lean supone un gran avance.
Para los desarrolladores, lo más amplio es que la demostración formal empieza a ser asequible. El artículo lo compara con seL4 y CompCert, verificados con años de trabajo experto sobre código escrito para ello. Herramientas como Lean LSP MCP, que analizamos, ya permiten a un agente de programación trabajar contra el verificador de Lean, y DeepMind publica sus propios artefactos de verificación.
Los límites están explicados. El alcance verificado es el código de sesiones uno a uno, no todo Signal. Las garantías simbólicas suponen una criptografía perfecta, y los resultados confían en el núcleo de Lean y en los contratos de algunas rutinas a las que llama el código. La propia DeepMind dice que escalar el método requiere más investigación. Y una demostración vale lo que vale la especificación que demuestra, por eso las especificaciones aprobadas por personas son lo que más merece una revisión externa.