DeepMind verifica con IA la criptografía de Signal

DeepMind verificó con IA la criptografía de Signal en cuatro semanas

Google DeepMind usó IA agéntica para demostrar matemáticamente, es decir verificar formalmente, varias de las garantías criptográficas clave del protocolo Signal, el mismo que protege las conversaciones en la app Signal, Google Messages y WhatsApp. El trabajo se completó en cuatro semanas como prueba de concepto y, según TechBooky, los agentes produjeron cerca de seis millones de líneas de prueba en Lean en ese periodo.

El dato que importa para un founder no es el hito criptográfico en sí, sino el método: lo que históricamente exigía años de trabajo de especialistas se comprimió a semanas con un framework de IA. Eso mueve el cálculo de costo-beneficio de asegurar software crítico.

¿Qué verificó DeepMind del protocolo Signal y qué quedó afuera?

El proyecto usó AlphaProof Code, un framework que combina agentes de IA con revisión humana. Los investigadores definieron qué propiedades querían probar y revisaron las especificaciones; los agentes se encargaron de construir y auditar las pruebas sobre el código real. Según ZDNET, los agentes marcaron apenas el 1% del código para una segunda revisión humana, lo que representó un ahorro de tiempo considerable.

Leíste lo que hace la IA. ¿Y en tu negocio?

Un agente de IA puede quedarse con parte de tu día: ordenar lo pendiente y pedirte el OK antes de actuar. El Kit «tu mano derecha con IA» trae un video de 11 minutos y una ficha para dejar al tuyo trabajando. CAR está cerrada por ahora; al anotarte, te avisamos cuando abra.

👥 Quiero el Kit →

Los límites del trabajo son tan importantes como el resultado:

No se verificó la app móvil completa de Signal, solo propiedades seleccionadas de la implementación criptográfica central.
El análisis no encontró vulnerabilidades nuevas en las porciones revisadas.
Para validar el método, los investigadores reintrodujeron dos bugs ya conocidos y corregidos de Signal en una versión aislada del código. El sistema los identificó y mostró que el protocolo no podía verificarse formalmente en ese estado.

Como señala TechBooky, probar que el código cumple una especificación no equivale a probar que la especificación cubre todas las amenazas. El sistema operativo del dispositivo, las actualizaciones, la recuperación de cuenta y el comportamiento del usuario quedan fuera del alcance verificado.

¿Por qué la verificación formal dejó de ser un lujo?

La verificación formal usa matemáticas para comprobar que el software hace lo que dice hacer, en lugar de testear casos puntuales. Durante décadas fue territorio de unos pocos sistemas críticos porque el costo humano era enorme: según WIRED, la prueba original del microkernel seL4 demandó cerca de 20 años-persona de trabajo experto para unas 8.700 líneas de código.

La IA está rompiendo ese cuello de botella. ZDNET reporta que el equipo de DeepMind hizo en un mes lo que normalmente llevaría años a especialistas. Y WIRED recoge el caso de la investigadora de Stanford Chuyue Sun, cuyo tool de IA completó un proyecto de ingeniería en menos de medio día y por menos de US$500, frente a los cinco meses que le tomó a tres expertos hacerlo a mano.

El escepticismo, sin embargo, es real y conviene escucharlo. Will Wilson, que dirige la startup de búsqueda de bugs Antithesis, describe la verificación formal como ‘una trampa’ y cuenta que su empresa gastó millones en verificar algunas de sus defensas de ciberseguridad, y aun así encontró errores adicionales con su propia herramienta. Vitalik Buterin lo resumió en un post: ‘la verificación formal no es una panacea’.

¿Hay negocio en verificar software con IA?

Sí, y se está formando rápido. &Truth, una public benefit corporation fundada a comienzos de 2026, salió del stealth el 29 de octubre de 2026 con US$70 millones en ronda seed para construir lo que llama una máquina universal de verificación de código, según WIRED y Unite.AI. Su apuesta es que la IA acelera el trabajo de prueba en 100x o más y que su tecnología de automatización suma otro 100x.

Harmonic, cofundada por el CEO de Robinhood Vlad Tenev, levantó US$295 millones y anunció que su agente matemático Aristotle ya soporta verificación de software escrito en C y diseños de hardware en Verilog; está evaluando la tecnología con posibles usuarios como Tensordyne y Nvidia, cuyo brazo de venture capital es inversor de la startup, según WIRED. En paralelo, Anthropic y la startup de verificación Theorem anunciaron que encontraron con IA bugs en software open source que billones de tests no habían detectado.

El contexto empuja en la misma dirección: Sundar Pichai afirmó que el 75% del código nuevo en Google ya es generado por IA y aprobado por ingenieros, y en septiembre de 2026 se publicaron 14.959 vulnerabilidades de software, 3,5 veces más que un año antes, de acuerdo con WIRED.

¿Qué significa esto para tu startup?

No necesitas verificar todo tu producto, ni podrías. La lección del caso Signal es que se puede empezar por lo que más duele si falla.

Elige uno o dos componentes críticos y verifícalos. Autenticación, cifrado, manejo de pagos o la lógica que decide permisos. DeepMind no verificó la app completa: verificó el núcleo criptográfico. Ese recorte es una estrategia, no una limitación.
Exige el alcance por escrito antes de creer en un ‘verificado’. Pregunta qué propiedades se probaron, sobre qué versión del código y bajo qué supuestos. Una prueba válida dentro de un modelo incompleto da una garantía más estrecha de lo que sugiere la palabra.
Trata la verificación como complemento del testing, no como reemplazo. Antithesis encontró bugs en software que sus propios clientes ya habían verificado formalmente. Los dos enfoques cubren cosas distintas.
No presupuestes todavía con precios de mercado. DeepMind hizo el análisis de Signal gratis como proyecto de investigación y Google se negó a compartir su costo y a comentar si lanzará un producto comercial. El precio de la verificación asistida por IA aún no está definido.

Conclusión

El trabajo de Google DeepMind sobre Signal es un hito doble: valida de forma independiente una criptografía que protege comunicaciones masivas y demuestra que la IA agéntica puede hacer viable algo que durante décadas fue prohibitivo. Swarat Chaudhuri, investigador de DeepMind, lo dijo sin adornos: ‘hay un largo camino por recorrer antes de poder escalar esto a todo el software del mundo, y queremos hacerlo’.

Para una startup, la lectura práctica es más modesta y más útil: la verificación formal dejó de ser exclusiva de NASA y Apple. Empieza por el componente que no puedes permitirte que falle, documenta el alcance y no confundas una prueba matemática con una garantía total.