AlphaProof Code de DeepMind verificó el protocolo criptográfico de Signal en 4 semanas

Cualquier desarrollador conoce esa sensación: las pruebas pasan, la revisión del código está aprobada, la auditoría no ha encontrado nada y, aun así, cuesta dormir tranquilo. Las pruebas comprueban escenarios concretos, y un fallo puede esconderse en uno que a nadie se le ocurrió. Para una aplicación web corriente, puede ser tolerable. Para la criptografía que protege la privacidad de millones de conversaciones, no.

Google DeepMind propone otra vía y ha lanzado AlphaProof Code, un sistema multiagente que automatiza la verificación formal del código.

Qué es la verificación formal, sin entrar en matemáticas

Imaginemos una función de ordenación. Las pruebas la comprobarán con un centenar de arrays. La verificación formal sigue otro camino. Primero se expresan las propiedades matemáticamente: el array de salida está ordenado y contiene los mismos elementos que el de entrada. Después se construye una demostración de que el código cumple esas propiedades para cualquier array, no solo para cien ejemplos.

Es el nivel más alto de garantías de seguridad. Pero casi nadie lo utiliza: el método es caro y lento, y hay muy pocos especialistas. A menudo, la demostración termina siendo más larga que el propio código y hay que escribirla a mano.

Qué hicieron exactamente con Signal

El equipo aplicó AlphaProof Code al código del protocolo criptográfico de Signal, que se utiliza para cifrar conversaciones en Signal y Google Messages. Los agentes basados en Gemini 4 Carbon escribieron más de seis millones de líneas en Lean, un lenguaje y un entorno de comprobación de demostraciones formales. El resultado es una demostración matemática de que el código ofrece las garantías de seguridad declaradas.

Aquí destacan dos cifras:

• 4 semanas. Según los autores, una tarea de esta magnitud suele llevar años a equipos de expertos.
• ~1%. Esa es la proporción de puntos que los propios agentes marcaron como necesitados de revisión humana tras auditar su demostración. El resto se completó sin intervención manual.

Google afirma que es la primera vez que se utiliza IA para verificar formalmente un programa real. Es una afirmación de la propia compañía; todavía no hay una verificación independiente.

Dónde está la trampa

Primero, los límites. Una demostración formal solo es tan sólida como su especificación. Si las propiedades están incompletas o no son las adecuadas, se demostrará que el código es correcto respecto de un objetivo equivocado. Por eso, «se ha demostrado su seguridad» debe leerse como «se ha demostrado que cumple unas garantías concretas definidas por escrito». No significa «es imposible vulnerarlo».

Otra salvedad: una demostración así no abarca todo lo que rodea al código. El entorno, el hardware, los errores de integración y el factor humano quedan fuera. La fuente tampoco revela el coste de ejecutar el sistema, los recursos de cómputo necesarios ni si estará disponible para todo el mundo. Por ahora es una demostración de investigación, no un producto que se pueda incorporar mañana.

El enfoque también tiene un punto fuerte. La demostración se comprueba automáticamente, de modo que no hace falta confiar en la palabra de los agentes ni de los autores. Si Lean acepta la demostración, es correcta. Las alucinaciones del modelo no son un problema aquí: un paso incorrecto simplemente no superará la comprobación.

Qué hacer con esto

Para quienes desarrollan código crítico (criptografía, pagos, núcleos de sistemas operativos, protocolos de consenso): conviene seguir de cerca cómo se abarata la verificación formal. Si otros proyectos confirman que puede llevar un mes en lugar de años, la barrera de entrada caerá drásticamente.

Para responsables de producto y fundadores del sector de la seguridad: en lugar de decir «hemos superado una auditoría», se podrá presentar una demostración matemática verificable. Es un argumento de peso para los sectores regulados y los clientes empresariales.

Para todos los demás: ya merece la pena acostumbrarse a formular los requisitos del código como propiedades verificables. Cuando los agentes aprendan a escribir las demostraciones, el cuello de botella será saber expresar con claridad qué debe cumplirse exactamente.

La conclusión principal es sencilla. Los agentes ya saben escribir código, y ahora empieza a surgir una forma de demostrar su corrección a una escala antes inalcanzable. Los autores creen que quizá sea la única manera de hacer frente a la velocidad y la escala de los ciberataques actuales. Es una afirmación discutible, pero la dirección está clara.