Google usa IA para verificar formalmente Signal
El 10 de noviembre de 2026, Google DeepMind presentó AlphaProof Code, una estructura de agentes de IA y revisión humana para comprobar formalmente propiedades de software complejo.
- Combina especificaciones revisadas por especialistas, agentes de IA y comprobación de pruebas en Lean.
- El proyecto examinó propiedades de seguridad seleccionadas del código de Signal e incluyó una prueba con fallos conocidos.
- Fuente y fecha: Google DeepMind, 10 de noviembre de 2026; el equipo responsable divulga los resultados.
Contexto y análisis de Noosigma AI
Resumen y contexto editorial elaborados a partir de la fuente indicada. Las afirmaciones y los resultados atribuidos a la organización son informes de la propia fuente; no constituyen una validación independiente de Noosigma AI.
En el trabajo sobre el protocolo Signal, especialistas definieron las propiedades de seguridad que debían demostrarse y revisaron las especificaciones matemáticas. Agentes basados en Gemini Carbon produjeron pruebas en Lean para partes del código real; el verificador del lenguaje comprueba mecánicamente cada prueba.
Por qué importa
El equipo informa que generó más de seis millones de líneas de Lean y completó el trabajo en cuatro semanas. El sistema también señaló una pequeña parte para revisión humana. En una prueba controlada, los investigadores reintrodujeron dos fallos ya corregidos en una copia aislada e informan que el método los detectó.
El resultado cubre las propiedades seleccionadas y formalizadas por los investigadores; no garantiza que se hayan cubierto todas las partes del protocolo ni todos los defectos. La descripción y la afirmación de prioridad histórica proceden de los autores y sus colaboradores. Fuente y fecha: Google DeepMind, 10 de noviembre de 2026.