AlphaProof Code demostró la corrección del núcleo de cifrado de Signal en 4 semanas en lugar de años

Las pruebas muestran que el código funciona con los datos de entrada que se te ocurrió comprobar. Para el cifrado eso no basta: un error que no se encontró en cinco años sigue siendo un error. Por eso, en los puntos más críticos se usa la verificación formal, es decir, la demostración matemática de la corrección. Funciona, pero es cara: requiere especialistas escasos y años de trabajo. DeepMind afirma haber encontrado la forma de reducir mucho ese plazo.

Qué mostró DeepMind

El equipo presentó AlphaProof Code, un sistema que demuestra que un programa cumple su especificación de seguridad sin errores. La demostración se hizo sobre el núcleo del protocolo de cifrado de Signal. Según los investigadores Pushmeet Kohli y Swarat Chaudhuri en el blog de DeepMind, un trabajo así suele llevar años, y aquí bastaron cuatro semanas.

Hay una segunda diferencia. Los intentos anteriores de verificar Signal se quedaban en el nivel del diseño teórico: demostraban que el protocolo en sí estaba bien concebido. AlphaProof Code verificó el código criptográfico real que se ejecuta en los dispositivos de los usuarios. Entre un esquema elegante y su implementación suelen esconderse los errores más desagradables, y esa es la brecha que aquí se cerró.

Cómo funciona, con un ejemplo sencillo

Imagina una función que suma dos números. Una prueba comprobará un par de decenas de combinaciones. La demostración en Lean funciona de otra manera: muestra que el resultado es correcto para cualquier valor de entrada, y Lean comprueba mecánicamente cada paso. Si el razonamiento tiene huecos, simplemente no pasará la verificación.

El proceso se divide en dos etapas:

• Primero, expertos humanos formulan los requisitos formales de seguridad: qué debe garantizar exactamente el código.
• Después, agentes de IA basados en Gemini Carbon ayudan a redactar las especificaciones y demuestran de forma independiente que el programa las cumple.

En total, los agentes escribieron más de seis millones de líneas en Lean. El sistema marcó alrededor del 1% de la base de código para revisión manual por parte de personas. Como control, los investigadores introdujeron dos errores en el código y ambos se detectaron de inmediato. El director técnico de Signal, Eren Kret, afirma que este enfoque refuerza la confianza en la privacidad de los datos ante las crecientes amenazas relacionadas con la IA.

Qué conviene tener presente

Primero: la demostración es tan correcta como la especificación. Si los expertos se equivocaron en los requisitos o se olvidaron de una clase de ataques, el sistema demostrará con toda honestidad el cumplimiento de un objetivo equivocado. El cuello de botella pasa de escribir demostraciones a formular requisitos, y no elimina a las personas.

Segundo: por ahora es una demostración en un solo proyecto, y la contó el propio desarrollador. El material no dice cuánto costó el cómputo ni con qué facilidad se puede trasladar el método a otro lenguaje y otra arquitectura. No hemos visto una evaluación independiente del resultado.

Tercero: un 1% del código en revisión humana parece poco, pero hablamos de criptografía, donde un solo fragmento sin verificar puede invalidar el resto. Marcar esas zonas es parte del método, no una debilidad.

Qué significa en la práctica

Para los desarrolladores, la señal principal es esta: se empieza a automatizar la parte más cara de la verificación, la escritura de demostraciones. La habilidad de formular requisitos precisos para el código, por ejemplo invariantes y límites del comportamiento admisible, será más valiosa que saber escribir demostraciones a mano. Si trabajas con criptografía, pagos o protocolos, conviene mirar Lean y herramientas similares ya.

Para los responsables de producto y los fundadores, es un nuevo argumento de confianza. La frase «el código está demostrado matemáticamente» es más fuerte que «hemos pasado una auditoría». Si el coste de la verificación realmente baja de años a semanas, ese argumento estará al alcance de más empresas que Signal.

DeepMind planea extender el método a redes eléctricas y dispositivos médicos mediante sistemas como CodeMender. Allí el coste de un error no es menor que en un mensajero, y los requisitos suelen ser más estrictos. Falta comprobar si el resultado se repite en otros proyectos y si lo confirman especialistas independientes.