DeepMind verificó formalmente en cuatro semanas las garantías clave del protocolo Signal

Las pruebas demuestran que el código funciona con los datos de entrada que se te ocurrió comprobar. La verificación formal responde a otra pregunta: ¿se puede demostrar matemáticamente que el código se comporta correctamente con cualquier dato? Los ingenieros llevan tiempo llamándola el santo grial de la seguridad, pero en la práctica las demostraciones se escribían a mano y requerían meses o años. Ahora DeepMind ha demostrado que buena parte de ese trabajo puede delegarse en un agente.

Qué se hizo exactamente

Investigadores de Google DeepMind verificaron formalmente, con ayuda del nuevo framework AlphaProof Code, una serie de garantías criptográficas clave del protocolo Signal. Este protocolo sustenta el cifrado en la aplicación Signal, Google Messages y WhatsApp. El proyecto fue una prueba de concepto y duró solo cuatro semanas.

Para valorar la velocidad, hay que entender en qué consiste el trabajo. Primero, las personas describen qué propiedades debe tener el código. Después, esa descripción se convierte en fórmulas. Y solo entonces se escribe la demostración propiamente dicha. La IA agéntica reduce mucho el tiempo precisamente en esta última etapa, la más laboriosa.

También hubo una comprobación práctica. El sistema no encontró nuevas vulnerabilidades en las partes del protocolo estudiadas. En cambio, en versiones antiguas de Signal con errores corregidos hace tiempo, AlphaProof Code halló esos problemas y mostró que ese código no puede verificarse formalmente. Para una herramienta de verificación es una prueba importante: no se limita a confirmar que "todo va bien", sino que realmente falla allí donde el código es erróneo.

Los investigadores no partieron de cero. Signal Foundation ya había hecho antes verificación formal de fragmentos de código más pequeños, y eso dio ventaja a DeepMind. El director técnico de Signal, Eren Kret, afirma que el enfoque de DeepMind permite ampliar notablemente el alcance de la verificación, lo que añade confianza en la privacidad de la implementación.

Por qué importa a los profesionales

El cambio principal está en el coste. La verificación formal era inaccesible para la mayoría de los equipos no porque nadie entendiera su utilidad, sino porque las demostraciones salían demasiado caras en tiempo humano. Si los agentes asumen la rutina, se amplía el conjunto de código que merece la pena demostrar. Pushmeet Kohli, de Google Cloud y DeepMind, habla abiertamente de bancos y otras empresas que podrán decir: "puedo demostrar estas propiedades".

Lo más sensato del proyecto es la organización del trabajo. Los agentes aportan y se autocorrigen casi en cada paso, pero en puntos clave solicitan la revisión de una persona. El investigador de DeepMind Swarat Chaudhuri explica por qué: no hace falta un "mundo vibe" en el que la IA genere por sí misma los objetivos, escriba por sí misma las demostraciones y, en esencia, apruebe exámenes que ella misma redactó. Hace falta un término medio.

Para el desarrollador se deduce algo sencillo. Una demostración vale exactamente tanto como la corrección de la especificación, es decir, de la descripción de lo que se considera comportamiento correcto. Si tanto la especificación como la demostración las escribe un modelo, obtienes un bonito papel sin garantías. La responsabilidad de formular los requisitos sigue siendo humana.

Limitaciones y qué hacer

Conviene mirar la escala con sobriedad. No se verificó toda la aplicación móvil de Signal, solo partes concretas del protocolo. El propio Chaudhuri reconoce que aún falta mucho para verificar todo el software del mundo. El sistema no encontró errores nuevos, así que por ahora es más una confirmación del trabajo ajeno que un descubrimiento.

La gran cuestión de la industria es la economía. DeepMind hizo el análisis gratis como proyecto de investigación, y Google no ha revelado el coste. La compañía también declinó comentar sobre un producto comercial o un servicio de verificación formal. Es decir, aún no hay un botón listo de "verificar mi código".

Lo que se puede hacer ya. Los investigadores publican la especificación y la demostración de Signal, un buen material de aprendizaje para quienes escriben código crítico: pagos, criptografía, infraestructura de confianza. Si trabajas en esos ámbitos, tiene sentido seguir cómo herramientas como AlphaProof Code pasan de demostración a producto, y aprender de antemano a formular propiedades del código de modo que puedan demostrarse. Esa habilidad, y no la de escribir demostraciones a mano, será previsiblemente la valiosa.