DeepMind prueba con IA la seguridad del código de Signal

DeepMind prueba con IA el código de Signal: seis millones de líneas y cuatro semanas

Google DeepMind guio a agentes de IA para generar más de seis millones de líneas de Lean —un lenguaje que las computadoras usan para comprobar demostraciones matemáticas— y probar formalmente las propiedades de seguridad del código real del protocolo Signal. Ese protocolo protege las conversaciones privadas de miles de millones de personas en Signal, Google Messages y WhatsApp.

Para un founder que hoy despliega código generado por IA más rápido de lo que puede revisarlo, el dato relevante no es el hito académico: es que la verificación formal, el estándar de seguridad más alto que existe, empieza a tener un camino automatizado. Y donde se destraba un cuello de botella de años, suele aparecer un mercado.

¿Qué verificó exactamente AlphaProof Code?

AlphaProof Code es un framework agéntico multi-LLM que reparte el trabajo de la verificación formal como lo haría un equipo de investigación: expertos humanos y modelos de IA deciden en conjunto qué hay que demostrar, y después un grupo de agentes hace las demostraciones.

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 →

Según el anuncio de DeepMind, los agentes —impulsados por Gemini Carbon— generaron más de seis millones de líneas de Lean. Luego auditaron su propia prueba y marcaron las zonas que necesitaban una segunda mirada humana: apenas el 1% del código, lo que liberó a los expertos para concentrarse donde el juicio humano aporta valor.

El detalle técnico que más importa: la mayoría de los esfuerzos de verificación de protocolos se detienen en el nivel del diseño. El equipo de DeepMind fue más allá y probó que el código compilado cumple propiedades de seguridad clave, como mantener los mensajes protegidos antes y después de que un dispositivo sea comprometido temporalmente. Ahí es donde suelen esconderse las vulnerabilidades reales: en la brecha entre el diseño y la implementación.

El proceso completo tomó cuatro semanas, una tarea que históricamente lleva años a equipos de especialistas. DeepMind lo presenta como la primera vez que se usa IA para verificar formalmente un protocolo criptográfico ampliamente desplegado con esta profundidad, y también como la primera vez que la implementación de un protocolo así se verifica formalmente por cualquier método, con o sin IA.

¿Cómo se sabe que el sistema detecta código con errores?

DeepMind hizo una prueba de control que vale la pena leer con atención: reintrodujo dos bugs reales y ya corregidos en una versión aislada del código de Signal. En ambos casos, el sistema produjo una prueba verificada por máquina de que la versión con errores era insegura.

Es decir, no solo confirma lo que está bien: también señala lo que está mal. Eso es lo que separa una demostración de marketing de una herramienta usable.

WIRED reportó que el análisis no encontró vulnerabilidades nuevas en las porciones del protocolo que revisó, y que los investigadores publicarán la especificación y la prueba que desarrollaron para que otros equipos las reutilicen. El mismo medio aclara el alcance: no se verificó la aplicación móvil completa de Signal.

¿Por qué esto importa más allá de Signal?

Los protocolos criptográficos sostienen casi toda la comunicación digital, desde la banca en línea hasta la navegación web. Un solo fallo puede exponer a millones de personas a la vez, y por eso los expertos llevan décadas analizándolos formalmente.

Ehren Kret, CTO de Signal, dijo en un comunicado que, mientras la verificación formal previa se concentraba en porciones más pequeñas del código, el enfoque de DeepMind permite una expansión significativa, y que verificar rigurosamente la implementación da mayor confianza en las garantías de privacidad del código.

Pushmeet Kohli, científico jefe de Google Cloud y vicepresidente de investigación de DeepMind, lo llevó al terreno corporativo: si puedes verificar la correctitud de estas implementaciones, puedes dormir tranquilo, y mencionó a los bancos y a todas las empresas que dependen de garantías y se preocupan por los bugs.

Pero hay dos preguntas abiertas que el propio equipo reconoce. Swarat Chaudhuri, investigador de DeepMind, dijo a WIRED que están muy entusiasmados con el resultado, pero que falta un largo camino antes de escalarlo a todo el software del mundo. Y Google declinó compartir el costo del análisis y no comentó si planea lanzar un producto o servicio comercial de verificación formal.

Traducción para un founder: la capacidad existe, el precio todavía no se conoce.

La verificación formal deja de ser un lujo

El contexto de mercado ayuda a dimensionar el momento. El 29 de octubre de 2026, la empresa de beneficio público &Truth salió de stealth con US$70 millones en capital semilla para construir lo que llama una máquina de verificación universal de código, con sede en Palo Alto y Singapur y construida sobre Lean y Mathlib, según reportó unite.ai.

En el ensayo que acompañó su lanzamiento, &Truth sostiene que la IA ya acelera el trabajo de prueba formal 100 veces o más y que su tecnología de automatización de pruebas lo acelera otro tanto, reduciendo la generación de pruebas de años o meses a horas o minutos. La misma compañía cita cifras que explican su urgencia: la prueba del microkernel seL4 tomó aproximadamente 20 años-persona de esfuerzo experto para unas 8.700 líneas de código, y en septiembre de 2026 se publicaron 14.959 vulnerabilidades de software, 3,5 veces más que un año antes.

También conviene ubicar a AlphaProof en su propia línea de tiempo. Como recordó Ars Technica, el sistema AlphaProof ya había igualado en 2024 el rendimiento de los medallistas de plata en la Olimpiada Internacional de Matemáticas, a un punto del oro. AlphaProof Code es el salto de las competencias de matemáticas al código que corre en producción.

¿Qué significa esto para tu startup?

No necesitas un equipo de investigación para sacar provecho de esta noticia. Necesitas cambiar el orden de tus prioridades.

Separa tu superficie crítica del resto. Nadie va a verificar todo su stack. Identifica el 5% del código donde un fallo sería catastrófico —autenticación, cifrado, pagos, permisos— y trátalo distinto. El ejercicio de DeepMind funcionó porque el alcance estaba acotado.
Escribe las especificaciones antes que las pruebas. El cuello de botella ya no es generar la demostración: es decidir qué hay que demostrar. Redacta en lenguaje claro las propiedades que tu sistema debe cumplir bajo cualquier input posible. Es el paso que los humanos no pueden delegar todavía.
No confundas tests con garantías. Los tests cubren los casos que se te ocurrieron; una prueba formal cubre todos los inputs bajo supuestos declarados. Si un cliente enterprise te pregunta cómo aseguras tu código, la respuesta de buena cobertura de tests va a sonar cada vez más débil.
Empieza por lo abierto. Lean y Mathlib son open source, y tanto DeepMind como &Truth dicen que liberarán sus especificaciones y librerías. Un equipo chico en LATAM o España puede experimentar con las mismas herramientas base sin presupuesto de laboratorio.
No presupuestes todavía. Google no reveló el costo del análisis de Signal y no hay producto comercial anunciado. Trata la verificación formal asistida por IA como una capacidad emergente: piloto, no línea de gasto.

Conclusión

DeepMind acaba de demostrar que un problema que consumía años de trabajo experto puede resolverse en semanas con un framework agéntico bien diseñado y revisión humana en los puntos correctos. Para el ecosistema startup, la señal es doble: por un lado, la seguridad de software deja de ser un problema exclusivamente de gigantes; por el otro, se abre una categoría de producto —verificación formal como servicio— donde todavía no hay ganador.

La pregunta que cada founder debería hacerse no es si su código es seguro, sino qué parte de su código podría probar matemáticamente si un cliente se lo exigiera mañana.