Qué pasó
- El 22 de octubre de 2026, Anthropic publicó con la empresa Theorem un trabajo en que Claude probó propiedades de seguridad en el código compilado de 123 bibliotecas de código abierto de OSS-Fuzz, con 239 puntos de entrada.
- Las pruebas demuestran que esos programas terminan sin errores de memoria ni aserciones fallidas para toda entrada menor a 64 MB, bajo supuestos: binario estático de un hilo, memoria fija, procesador RISC-V y Linux.
- Suman cerca de 180 millones de líneas en el lenguaje Rocq. Una prueba típica ronda las 600.000 líneas para binarios con una mediana de 18.000 instrucciones.
- En el proceso, Claude encontró fallas que habían escapado a billones de ejecuciones de pruebas, entre ellas una lectura fuera de límites, y volvió a detectar la falla CVE-2026-56132 en libexpat.
Por qué importa
- La verificación formal era un lujo: según Anthropic, implementar el núcleo seL4 tomó dos años-persona y verificarlo, 20. Si ese costo cae, puede llegar a bibliotecas que usa cualquier aplicación.
- Una prueba no es un parche. Garantiza solo las propiedades demostradas y bajo los supuestos declarados; un binario multihilo o con otra memoria queda fuera.
- Para equipos de desarrollo, Theorem ofrece correr el mismo proceso en otros proyectos abiertos y publica una skill de Claude para empezar.
El dato
180 millones. Líneas de pruebas en Rocq que generó el proyecto.
Contexto
Anthropic describe otros ensayos. Claude escribió una especificación formal del formato zlib y probó que la implementación del núcleo Linux la cumple. También desarrolló un intérprete de Python en Rust que coincidió con CPython en 99,95% de 1,7 millones de programas aleatorios.
Qué viene
- Anthropic publica un subconjunto de las pruebas y retiene las que podrían revelar fallas sin parche.
- La compañía dice que Opus 5.5 resuelve la mitad de 36 tareas de verificación con cerca de 40% menos tokens que Opus 5.
Cierre
PHP corrigió dos fallas de ejecución remota estancadas por dos años, dimensionadas con IA. Y Cisco documentó un malware que recibe órdenes de varios modelos de IA: el mismo cómputo sirve para atacar y para probar que un código resiste.
Fuentes
- Anthropic — LLMs are making formal software verification feasible at a much larger scale (22 de octubre de 2026)
- Imagen de portada: Derrick Coetzee (User:Dcoetzee), CC0, vía Wikimedia Commons
Editado por Rodrigo Cornejo. Quiénes escriben las notas
