El Frontier Red Team de Anthropic publicó el 22 de octubre una investigación en la que Claude escribió pruebas formales para 239 puntos de entrada de 123 bibliotecas de código abierto: mientras la entrada sea menor de 64 MB, estos programas no se bloquean. Las pruebas se asientan directamente sobre los ejecutables RISC-V compilados, con Theorem, una empresa de herramientas de verificación formal, como socio. Según Anthropic, es la primera vez que una IA realiza verificación formal a gran escala en el nivel de ensamblador de software de producción.
Todas las bibliotecas proceden del proyecto OSS-Fuzz de Google, es decir, ese conjunto de componentes básicos que lleva mucho tiempo en la plataforma de fuzzing; hay compresión, decodificación de imágenes y análisis de HTTP. Todo el proyecto llevó unas semanas.
Convertir el fuzzing en teoremas
El método tiene tres pasos. Primero, el equipo reescribió la batería de pruebas de fuzz existente de cada biblioteca como una especificación formal, que viene a decir: “este código de prueba no se bloquea con ninguna entrada”. La especificación se apoya en los modelos de semántica de instrucciones RISC-V y de semántica de procesos de Linux que aporta Theorem.
En el segundo paso, Claude escribe la prueba y el verificador de pruebas Rocq la comprueba línea por línea.
“Claude writes the proof; the Rocq kernel checks it against the specification.” (Claude escribe la prueba; el núcleo de Rocq la comprueba contra la especificación.)
El tercer paso trata los casos en que la prueba no avanza. Que una prueba se atasque suele indicar que de verdad hay un defecto en el código; entonces el propio Claude modifica el código, la especificación se regenera y se sigue demostrando. El equipo reconoce que este paso es propenso al “reward hacking”: el modelo podría alterar el programa a la ligera solo para que la prueba salga adelante. Por eso se añadió una penalización a los parches, se exige demostrar el rango de entradas que cada parche afecta, y todo se registra uno por uno y se audita manualmente.
Una prueba típica ronda las 600.000 líneas. Lo único en lo que al final hay que confiar son los modelos de semántica de RISC-V y Linux, el enunciado del propio teorema y el verificador Rocq.
Fallos descubiertos durante las pruebas
En el curso de las demostraciones se encontraron y corrigieron cientos de fallos, algunos de los cuales cuesta dar con ellos mediante fuzzing. El artículo menciona varios ejemplos: un subdesbordamiento de contador en un descompresor, que solo se activa con ciertas entradas de unos 20 MB; una lectura fuera de límites en un decodificador de imágenes, que requiere 64 MB de entrada y más de 2 GB de memoria; y otra lectura fuera de límites que exige que dos handles operen sobre el mismo archivo en un orden concreto. La CVE-2026-56132 de libexpat también fue redescubierta.
La prueba de cpp-httplib tuvo un obstáculo adicional: la recursión al destruir un std::set puede provocar un desbordamiento de pila. Para descartarlo, el equipo demostró a nivel de código máquina que el algoritmo de equilibrado del árbol rojo-negro de libc++ mantiene la profundidad del árbol en escala logarítmica.
La misma investigación incluye además algunos experimentos paralelos. Claude escribió en Rust un subconjunto de Python y, con Verus, demostró que respeta la semántica de CPython; en 1,7 millones de programas aleatorios, el comportamiento coincidió con CPython en un 99,95%. También generó por su cuenta una semántica de instrucciones x86 que, ejecutada paso a paso, es capaz de arrancar el espacio de usuario de Ubuntu, y de paso detectó cientos de errores en la documentación de referencia oficial.
Para comparar: seL4
La verificación formal no es nueva en la industria; la dificultad siempre ha estado en la mano de obra. En el sector se cita a menudo el microkernel seL4: unas diez mil líneas de C, con un esfuerzo de prueba que suele cifrarse en torno a veinte años-persona. El compilador CompCert siguió una vía parecida, pulido durante años por un equipo reducido. Lo que tienen en común estos proyectos es pocos objetos, ciclos largos y muchos expertos.
La escala de Anthropic esta vez fue de 123 bibliotecas en unas semanas; en una comparación aproximada, la estructura de costes por unidad de trabajo ha adoptado otra forma, y las personas pasan de escribir pruebas a definir especificaciones y revisar parches. El coste se ha trasladado a los tokens: el artículo dice que una prueba completa puede consumir cientos de millones de tokens. En las 36 tareas pequeñas, cada tarea daba a un único agente tres intentos con un presupuesto de 5 millones de tokens cada uno; al permitir que los agentes reutilizaran las pruebas de los demás, los tokens necesarios bajaron otro 17%.
La solidez de las garantías tampoco está en el mismo nivel. seL4 demuestra corrección funcional; aquí solo se demuestra “no bloquearse”, un alcance mucho más estrecho.
Los huecos más allá de la prueba
Las limitaciones que enumera la propia Anthropic son bastante concretas. Las pruebas se basan en binarios RISC-V de un solo hilo, enlazados estáticamente y con musl libc, mientras que la mayoría de los usuarios ejecuta versiones en x86 o ARM con glibc enlazada dinámicamente. AddressSanitizer por sí solo no detecta todos los errores de seguridad de memoria, hay puntos de entrada sin cubrir, y la corrupción de memoria causada por un uso indebido de la biblioteca por parte del llamante también queda fuera de la prueba.
“Formally verified” does not mean “bug-free.” (“Verificado formalmente” no significa “sin bugs”.)
La desviación entre la especificación y la máquina real es el punto donde este camino más fácilmente falla. Rocq y los modelos de semántica también necesitan endurecerse, algo que el artículo califica de “no trivial”. La valoración del equipo es que la verificación formal se convertirá en una etapa habitual del desarrollo de software seguro; en cuanto a cuándo estas pruebas alcanzarán entornos de despliegue mayoritarios como x86 y glibc, el artículo no da fecha.
Fuentes: artículo de investigación del Frontier Red Team de Anthropic, CocoLoop; la página de investigación de Anthropic se usó para contrastar el número de bibliotecas, puntos de entrada, líneas de prueba y el criterio de comparación de tokens.