Claude escribe 180 millones de líneas de prueba matemática en la primera verificación formal de IA a gran escala de software de código abierto

Informe completo

Anthropic anunció en su página oficial de investigación el 22 de octubre: en colaboración con la empresa de verificación de software Theorem, Claude verificó formalmente las propiedades de seguridad en el nivel de ensamblaje RISC-V en 123 bibliotecas de código abierto del mundo real extraídas de OSS-Fuzz de Google, que cubren 239 puntos de entrada del programa. La compañía lo llama "el primer esfuerzo a gran escala para utilizar IA para aplicar verificación formal al software de producción a nivel de código ensamblador".

La escala es sorprendente: alrededor de 180 millones de líneas de pruebas Rocq, con una prueba típica de unas 600.000 líneas, que cubren binarios con una longitud media de 18.000 instrucciones RISC-V, todo completado en cuestión de semanas. El kernel de Rocq verifica de forma independiente cada prueba, por lo que no es necesaria una revisión manual línea por línea.

El método convierte las pruebas fuzz existentes en especificaciones matemáticas: para cualquier entrada de menos de 64 MB, un binario RISC-V vinculado estáticamente de un solo subproceso en Linux siempre debe salir normalmente, sin violaciones de seguridad de la memoria. Cuando Claude sospechó que había un error a mitad de prueba, parcheó el código directamente y volvió a probar la nueva especificación.

Cientos de errores surgieron a lo largo del camino, incluido un contradesbordamiento en una copia del descompresor que provocaba una escritura fuera de límites (activable solo por entradas de ~20 MB con un diseño poco común), una lectura fuera de límites en un decodificador de imágenes y un redescubrimiento de CVE-2026-56132 en libexpat; algunas vulnerabilidades habían estado al acecho durante años.

Anthropic reconoce los límites en sí: una verificación formal aprobada no significa que esté libre de errores: las pruebas cubren solo binarios RISC-V estáticos de un solo subproceso, mientras que la mayor parte del código en realidad se ejecuta en x86/ARM. Ha publicado un subconjunto de pruebas en GitHub para verificación independiente, y Theorem dice que ejecutará el mismo proceso para otros proyectos de código abierto.

Los resultados secundarios también son notables: se demostró que la implementación zlib del kernel de Linux cumple con RFC 1950 en el nivel binario x86, y un gran subconjunto de un intérprete de Python escrito en Rust coincidió con el comportamiento de CPython en el 99,95% de más de 1,7 millones de programas aleatorios.