Claude demuestra con pruebas formales que 123 librerías abiertas no fallan y halla cientos de errores
Anthropic y Theorem usan IA para verificar código de software libre con pruebas matemáticas revisadas por una herramienta automática.
Anthropic y Theorem han usado Claude para escribir pruebas matemáticas de que el código compilado de 123 librerías de código abierto no se bloquea con entradas de menos de 64 MB. En el proceso encontró «cientos de errores».
Datos clave
Anthropic publicó el 22 de octubre de 2026, junto con la empresa Theorem, una investigación en la que Claude escribió pruebas formales (demostraciones matemáticas verificables por máquina) sobre código de librerías de software libre del proyecto OSS-Fuzz.
Las pruebas trabajan sobre el código ya compilado para RISC-V (un tipo de procesador), no sobre el código fuente. Se convirtieron las pruebas de fuzzing, que lanzan entradas aleatorias para provocar fallos, en especificaciones, y Claude demostró que esas pruebas no bloquean el programa con ninguna entrada de menos de 64 MB. Un comprobador de pruebas llamado Rocq validó los resultados.
En total son 123 librerías, 239 puntos de entrada y unos 180 millones de líneas de pruebas. Durante el proceso Claude descubrió «cientos de errores» y parcheó los que encontró.
Anthropic advierte de las limitaciones: «verificado formalmente» no significa «sin errores», porque las pruebas valen lo que valgan la especificación y los modelos del procesador y del sistema. Además suponen un programa de un solo hilo sobre RISC-V con Linux y la librería musl, mientras que la mayoría de la gente usa x86 o ARM, y no cubren a quien use mal la librería.
«Most software is riddled with bugs, which AI can now easily find and exploit.»
Qué significa para ti
- No cambia nada en tus aplicaciones hoy, pero apunta a que la IA se usará para reforzar el software, no solo para atacarlo.
- Sigue actualizando tus programas: la verificación formal cubre solo una parte pequeña del software que usas.
Para aprovecharlo
Fuentes
¿Ves un error? Avísanos y lo corregimos en la fe de erratas.