Anthropic usa Claude para verificar formalmente 123 librerías de código abierto y encuentra fallas que llevaban años ocultas

Anthropic informó el 22 de octubre que Claude demostró matemáticamente, a nivel de código de máquina RISC-V, que 239 funciones de 123 librerías de código abierto no pueden caerse con entradas de menos de 64 MB. Las pruebas suman unos 180 millones de líneas en el lenguaje Rocq, se hicieron en pocas semanas junto a la empresa Theorem y en el camino aparecieron cientos de errores, algunos invisibles por años pese a pruebas intensivas. Opus 5.5 usó cerca de 40% menos tokens que Opus 5 en 36 tareas de verificación.