Claude demuestra la seguridad de 123 bibliotecas a nivel de código RISC-V

Anthropic y la compañía Theorem han publicado los resultados de un proyecto en el que Claude escribió, de forma autónoma, pruebas formales de corrección para código open source real. El modelo demostró la ausencia de fallos en 239 puntos de entrada de 123 bibliotecas de Google OSS-Fuzz. Las pruebas no trabajan con el código fuente, sino con instrucciones RISC-V ya compiladas, y suman en total unos 180 millones de líneas en Rocq. Hasta ahora, un trabajo así exigía años de esfuerzo de especialistas muy escasos, por lo que solo se aplicaba donde un error resulta demasiado caro, por ejemplo en la aviónica de Airbus.

El test de fuzzing como especificación ya hecha

El principal problema de la verificación formal es que primero hay que explicar qué significa «correcto». Para un decodificador PNG existe el RFC 2083, pero para un editor de texto o un navegador no hay una especificación clara. Los investigadores lo resolvieron aprovechando los tests de fuzzing que ya tenían los desarrolladores: convirtieron la condición «el test nunca falla» en una especificación formal. La describieron sobre un modelo de cómo se ejecuta en Linux cualquier binario para RISC-V.

El fuzzer prueba un enorme número de entradas semialeatorias, pero no garantiza una cobertura completa. La prueba, en cambio, sí ofrece una garantía: si Claude demostró que el test no fallará con ninguna entrada de menos de 64 MB, el fuzzing de ese punto de entrada en RISC-V ya no encontrará nada más. OSS-Fuzz compila los programas en C y C++ con AddressSanitizer, así que cualquier acceso incorrecto a la memoria cuenta como un fallo. Por eso la propiedad demostrada incluye automáticamente la memory safety, la principal fuente de vulnerabilidades.

Qué se logró exactamente

El proyecto duró varias semanas. El criterio de éxito era que Claude escribiera la prueba y que la comprobara el núcleo de Rocq, de modo que una persona no tuviera que leer cientos de miles de líneas. Hay que confiar en tres cosas: los modelos formales de RISC-V y de los procesos de Linux, las formulaciones exactas de los teoremas y el propio Rocq.

• 123 bibliotecas de OSS-Fuzz, 239 puntos de entrada
• unos 180 millones de líneas de Rocq; una prueba típica ronda las 600 mil líneas
• binario mediano: 18 000 instrucciones RISC-V
• garantía: salida correcta sin errores de memoria ni fallos de assertions con cualquier entrada de hasta 64 MB
• supuestos: binario estático de un solo hilo, presupuesto de memoria fijo, RISC-V y Linux

Los propios autores subrayan que esto no significa que las bibliotecas carezcan de bugs. Los errores restantes pueden esconderse en los componentes de confianza o fuera de la propiedad demostrada. Sin embargo, la superficie de verificación se reduce: para cubrir proyectos nuevos no hace falta ampliar la base de confianza.

Bugs que el fuzzer no habría encontrado

Cuando una prueba no cerraba, Claude corregía el código, se regeneraba la especificación y el modelo demostraba la nueva versión. Así aparecieron cientos de errores. El fuzzer casi seguro no habría detectado muchos de ellos, porque muta entradas pequeñas, normalmente de hasta 1 MB. Algunos ejemplos:

• un underflow de un contador en una copia de un descompresor, que lleva a una escritura fuera de los límites del búfer, solo con entradas de unos 20 MB de estructura poco habitual
• una lectura fuera de límites en un decodificador de imágenes, que requiere una entrada de 64 MB o más y más de 2 GB de memoria
• una lectura fuera de límites en otra biblioteca tras una secuencia concreta de llamadas a través de dos descriptores del mismo archivo
• el redescubrimiento de CVE-2026-56132 en libexpat, que requiere un anidamiento profundo
• un error lógico sin fallos: la función que limita los archivos cargados no funcionaba siempre

Hay también un efecto secundario importante: incluso un intento de prueba fallido saca a la luz defectos reales. Además, los tests de fuzzing suelen comprobar propiedades de alto nivel, por ejemplo la codificación y decodificación sin pérdidas. En el algoritmo de compresión LZO, el test afirma que descomprimir los datos comprimidos devuelve el original. Si la propiedad se incumple, el programa falla, y demostrar que no hay fallos equivale a demostrar la propia propiedad. En cpp-httplib, Claude tuvo que descartar por separado un desbordamiento de pila causado por una recursión profunda en el destructor de std::set.

Conclusión práctica para los equipos

El contexto del trabajo es exigente: en el kernel de Linux se han revelado recientemente más de 1000 vulnerabilidades, y los modelos son cada vez mejores encadenando pequeños bugs en cadenas de exploits. Como comparación, la implementación del kernel seL4 costó dos personas-año y su verificación, veinte. Si el coste de las pruebas baja a medida que crecen las capacidades de los modelos, y las pruebas ya hechas pueden reutilizarse entre bases de código, la economía cambia.

Anthropic publica parte de las pruebas, los modelos de RISC-V y del SO, así como las especificaciones de los tests que no se lograron demostrar. Theorem propone ejecutar el mismo pipeline en otros proyectos open source y lanza un Claude skill para verificar por cuenta propia. Los desarrolladores que probaron en su día métodos formales con modelos más débiles y los abandonaron deberían volver a plantearse la cuestión. Lo razonable es empezar por un proyecto que ya cuente con buenos tests de fuzzing: allí la especificación está casi lista. En paralelo, los autores están probando los mismos métodos en zlib y en la verificación de la equivalencia de comportamiento de un intérprete de Python escrito en Rust.