Anthropic afirma que Claude escribió pruebas formales de que 123 bibliotecas de código abierto no pueden bloquearse

En colaboración con Theorem, Anthropic afirma que usó Claude para demostrar propiedades de seguridad a nivel de ensamblador (RISC-V) en más de 100 bibliotecas de código abierto de uso real, en lo que califica como el primer uso de la IA a gran escala para verificar formalmente software de producción a ese nivel.

Según Anthropic:

• Qué se demostró: para 239 puntos de entrada de pruebas de fuzzing distribuidos en 123 bibliotecas de OSS-Fuzz, los programas siempre terminan con normalidad, sin errores de seguridad de memoria ni aserciones fallidas, para cualquier entrada de menos de 64 MB. Esto se cumple bajo ciertos supuestos: un binario estático de un solo hilo, con un límite de memoria fijo, en una CPU RISC-V que ejecuta Linux. Las pruebas suman unos 180 millones de líneas de Rocq, verificadas por el comprobador de pruebas de Rocq.
• Cómo: cada prueba de fuzzing existente de las bibliotecas se convirtió en una especificación («esta prueba nunca se bloquea»), y Claude escribió la demostración, corrigiendo los errores que encontraba por el camino. Anthropic afirma que esto permitió encontrar cientos de errores, incluidos algunos a los que probablemente un fuzzer no llegaría, como una escritura fuera de límites que requiere una entrada inusual de 20 MB, y el redescubrimiento de CVE-2026-56132 en libexpat.
• Otros experimentos: Claude demostró que la implementación de zlib del kernel de Linux coincide con una especificación de RFC 1950 a nivel del binario x86, y creó un intérprete de Python en Rust cuyo comportamiento coincidió con el de CPython en el 99,95 % de 1,7 millones de programas aleatorios. Anthropic también afirma que los intentos de verificación formal de un lector de PDF muy utilizado sacaron a la luz en una semana tantos errores de seguridad como los que suelen notificarse en un año.
• Costo: las pruebas pueden requerir cientos de millones de tokens. En 36 tareas pequeñas de verificación, Anthropic afirma que Opus 5.5 demuestra la mitad con alrededor de un 40 % menos de tokens que Opus 5, y que los agentes que compartían pruebas necesitaron un 17 % menos de tokens.

Anthropic está publicando una parte de las pruebas y la semántica de RISC-V y Linux. Theorem ofrece ejecutar el mismo proceso para otros proyectos de código abierto y está publicando una skill de Claude para verificar tu propio código. Anthropic señala que esto no demuestra que las bibliotecas estén libres de errores: los errores restantes estarían en los componentes de confianza o fuera del alcance de las pruebas.