Verificación formal con Claude: pruebas para 123 bibliotecas de código abierto

El 22 de octubre, el equipo Frontier Red Team de Anthropic, junto con la empresa Theorem, publicó un estudio en el que Claude escribió pruebas formales de seguridad para 123 bibliotecas de código abierto del proyecto OSS-Fuzz. Las pruebas se refieren al código RISC-V compilado, no al código fuente. Según los autores, es la primera verificación formal de software de producción a nivel de ensamblador con IA a esta escala.

¿Cómo funciona la verificación formal con Claude?

La verificación formal es una demostración matemática de que un programa tiene una propiedad concreta para cualquier entrada posible, no solo para las que alguien probó. El problema es que hasta ahora exigía años de trabajo de expertos. Una comparación del estudio: verificar el kernel seL4 llevó unos 20 años-persona, y escribirlo, dos.

El pipeline del estudio es así:

1. El punto de partida son las pruebas de fuzzing existentes de OSS-Fuzz (un proyecto de Google que bombardea sin parar las bibliotecas con datos aleatorios).
2. La biblioteca, junto con la prueba, se compila en un ejecutable RISC-V.
3. A partir de la semántica del procesador RISC-V y de un proceso de Linux elaborada por Theorem, se genera automáticamente una especificación: el programa debe terminar siempre con normalidad, sin errores de memoria ni aserciones fallidas.
4. Claude escribe la prueba y el verificador de Rocq confirma que cumple la especificación.
5. Cuando Claude encuentra un error, parchea el código, la especificación se regenera y la prueba se construye de nuevo desde cero.

La garantía cubre cualquier entrada de menos de 64 MB y cualquier respuesta del sistema y disposición de memoria modeladas (suponiendo un programa estático y de un solo hilo en RISC-V y Linux).

¿Qué cifras dio Anthropic?

1. 239 puntos de entrada en 123 bibliotecas.
2. En total, unos 180 millones de líneas de pruebas en Rocq; una prueba típica tiene unas 600 000 líneas y abarca un programa con una mediana de 18 000 instrucciones RISC-V.
3. Todo llevó unas pocas semanas.
4. En 36 tareas pequeñas, Opus 5.5 demostró la mitad consumiendo alrededor de un 40 % menos de tokens que Opus 5, y los agentes que trabajaban en un espacio compartido consumieron un 17 % menos que en solitario.

Curiosamente, la prueba para cpp-httplib exigió demostrar que el árbol rojo-negro de libc++ tiene una profundidad acotada logarítmicamente, porque era la única forma de descartar un desbordamiento de pila en el destructor de std::set.

¿Qué errores encontró Claude?

Según los autores, el proceso destapó cientos de errores que habían sobrevivido a años de fuzzing. Ejemplos de la publicación:

1. Un desbordamiento negativo de un contador en un descompresor que provocaba una escritura fuera del búfer, pero solo con una entrada de unos 20 MB con una estructura poco habitual.
2. Una lectura fuera del búfer en un decodificador de imágenes que requería una entrada de 64 MB y más de 2 GB de memoria.
3. Una lectura fuera del búfer que solo aparecía con una secuencia concreta de llamadas sobre dos descriptores del mismo archivo.
4. El redescubrimiento de CVE-2026-56132 en libexpat (requería una entrada profundamente anidada).
5. Un error lógico: una función que restringía el acceso a archivos no siempre funcionaba, aunque nada fallaba.

A eso se suman tres experimentos adicionales. Claude escribió una especificación formal de RFC 1950 y demostró sobre binarios x86 que el zlib del kernel de Linux la implementa correctamente. También construyó en Rust un intérprete de un subconjunto de Python que, en 1,7 millones de programas aleatorios, se comportó como CPython en el 99,95 % de los casos. Y un intento de verificar un lector de PDF popular encontró en una semana tantos fallos de seguridad como los que suelen notificarse en un año.

Es la misma dirección que en PHP2Shell y en Claude Mythos en Bank of America: los modelos de IA encuentran errores que personas y herramientas clásicas pasaron por alto durante años. Solo que esta vez no termina únicamente en un parche, sino en una prueba.

¿A qué prestar atención?

Primero, a lo que significa «verificado». Los autores lo dicen claramente: la verificación formal no significa código sin errores (en el original, «»Formally verified« does not mean »bug-free.«»). Una prueba es tan buena como la especificación, los modelos de RISC-V y Linux y el propio verificador de Rocq.

Segundo, al alcance. Las pruebas cubren binarios RISC-V estáticos y de un solo hilo con musl, mientras que la mayoría ejecutamos código en x86 o ARM con glibc. Tampoco cubren el código muerto ni los casos en que es el programa que llama a la biblioteca el que corrompe la memoria.

Tercero, al coste. Algunas pruebas pueden consumir cientos de millones de tokens, algo que los propios autores señalan como la principal limitación.

Parte de las pruebas ya está en GitHub (oss-verify-proofs), junto con la semántica de RISC-V y Linux. El resto espera, porque podría revelar errores sin parchear.

FAQ

¿Qué es la verificación formal?

Es una demostración matemática, comprobada por un programa, de que el código tiene una propiedad concreta para todas las entradas; por ejemplo, que nunca escribe fuera del búfer. Las pruebas y el fuzzing solo comprueban casos seleccionados.

¿Las bibliotecas verificadas están libres de errores?

No. La prueba garantiza la ausencia de fallos solo dentro del modelo descrito (RISC-V, Linux, entrada de menos de 64 MB, un solo hilo). Los errores pueden estar en la especificación, en el modelo de la máquina o fuera de ese alcance.

¿Puedo verificar mi propio proyecto?

Theorem gestiona OSS Verify, un programa gratuito para proyectos de código abierto seleccionados. Lo solicita el mantenedor del proyecto mediante un pull request con los archivos project.yaml, Dockerfile y build.sh, de forma parecida a OSS-Fuzz. Hay que contar con trasladar el build a binarios estáticos riscv64.