Anthropic: Claude ya ha realizado una verificación formal a gran escala de bibliotecas de código abierto

El 22 de octubre, el equipo Frontier Red Team de la empresa de inteligencia artificial Anthropic publicó un estudio que revela que los modelos de lenguaje grande (LLM) ya poseen la capacidad de generar automáticamente pruebas formales a gran escala. En colaboración con Theorem, el equipo llevó a cabo una verificación formal de propiedades de seguridad sobre más de 100 bibliotecas de código abierto reales, a nivel de ensamblador RISC-V, utilizando modelos Claude. Se trata de la primera vez que un sistema de IA realiza una verificación formal a gran escala sobre software de producción directamente en el nivel de ensamblador. Durante la construcción de dichas pruebas, el equipo descubrió accidentalmente múltiples vulnerabilidades de seguridad que habían pasado desapercibidas durante mucho tiempo. El método experimental consistió en transformar casos de prueba *fuzz* compilables ya existentes en Google OSS-Fuzz en especificaciones formales, y luego ejecutar la verificación sobre entradas de tamaño arbitrario —hasta 64 MB— bajo restricciones como un entorno estático binario de un solo hilo, un presupuesto fijo de memoria, una arquitectura de CPU RISC-V y un entorno de ejecución Linux.