Anthropic informó que su modelo Claude verificó formalmente propiedades de seguridad en 123 bibliotecas de software abierto y que en el proceso encontró cientos de errores. Algunas de esas fallas habían escapado durante años a billones de ejecuciones de pruebas automáticas.

El proyecto se hizo junto a Theorem, una empresa de verificación de software, y aplica pruebas matemáticas directamente sobre el código de máquina ya compilado. Según los investigadores, el método puede hacer viable la verificación rigurosa en muchos más proyectos que hoy.

El trabajo apunta a un problema de seguridad que crece. Las herramientas automáticas ya encuentran vulnerabilidades en software maduro, y eso deja a los desarrolladores buscando formas más firmes de impedir fallas explotables. La verificación formal es una respuesta posible, porque demuestra que el código cumple ciertas reglas bajo condiciones definidas.

¿Cómo encontró Claude los errores ocultos?

Las pruebas tradicionales ejecutan un programa con entradas escogidas para que aparezcan las fallas. Las herramientas de fuzzing generan enormes cantidades de entradas inusuales, pero no alcanzan a cubrir todas las combinaciones posibles.

Anthropic usó Claude para convertir pruebas de fuzzing ya existentes en especificaciones matemáticas. Después, el modelo generó pruebas que demuestran que 239 puntos de entrada de programas, repartidos en las 123 bibliotecas, no se caen bajo las condiciones definidas.

Los investigadores trabajaron con código ensamblador RISC-V, que representa las instrucciones que ejecuta el procesador. Claude generó cerca de 180 millones de líneas de código de prueba, y una prueba típica ocupa unas 600.000 líneas.

Una herramienta aparte, llamada Rocq, revisó las pruebas contra sus especificaciones. Gracias a ese paso de verificación independiente, los desarrolladores no necesitan revisar a mano cada línea de prueba generada. Anthropic también dejó que Claude corrigiera los errores que encontraba durante la verificación, y luego el modelo generó pruebas nuevas para el código ya corregido.

Fallas que sobrevivieron años de pruebas

El proceso destapó vulnerabilidades que al fuzzing convencional le costaría encontrar. Una biblioteca tenía un desbordamiento por debajo en un contador que podía provocar una escritura fuera de límites durante la descompresión.

Para que esa falla apareciera hacía falta una entrada de unos 20 MB con una disposición de datos poco común. Otro error estaba en un decodificador de imágenes y solo se manifestaba con una entrada de 64 MB y más de 2 GB de memoria.

Claude también encontró una lectura fuera de límites que dependía de una secuencia específica de operaciones con dos manejadores abiertos sobre el mismo archivo. En otro caso redescubrió una vulnerabilidad ya conocida en libexpat, el analizador de XML.

No todos los problemas provocaban una caída. El modelo también identificó una falla lógica que podía permitir que una aplicación se saltara una función pensada para restringir qué archivos podía cargar.

Los hallazgos muestran que la verificación formal detecta defectos que las pruebas de rutina no ven. El método además permite demostrar propiedades para todas las entradas permitidas, algo que una prueba común no consigue.

¿Qué no garantizan las pruebas?

Anthropic advirtió que el software verificado formalmente no queda automáticamente libre de errores. Las garantías cubren solo las propiedades, entradas y supuestos que describe cada prueba.

El trabajo actual abarca programas RISC-V de un solo hilo, enlazados estáticamente y ejecutados sobre un entorno Linux modelado. La mayoría de los sistemas en producción usan otras arquitecturas de procesador o configuraciones de software distintas.

Las especificaciones tampoco garantizan propiedades que no describen. Los investigadores tienen que asegurarse de que sus modelos matemáticos representen con fidelidad a los procesadores y sistemas operativos reales.

Anthropic espera que modelos mejores y pruebas reutilizables bajen el costo de revisar componentes de software sensibles. Su argumento es que una biblioteca de uso masivo se verifica una vez y esa garantía la heredan todas las aplicaciones que dependen de ella.