En un informe publicado el 22 de octubre de 2026, Anthropic explicó que Claude y Theorem produjeron pruebas formales, comprobadas por Rocq, para 239 puntos de entrada de 123 bibliotecas de Google OSS-Fuzz. El resultado se limita a demostrar que esos puntos no provocan un fallo con entradas inferiores a 64 MB dentro de un modelo concreto de RISC-V y Linux; no cubre el comportamiento completo de cada biblioteca.
Cómo se pasa de una prueba fuzz a un teorema
El fuzzing consiste en ejecutar un programa con muchas entradas generadas para buscar fallos. Anthropic describió un paso adicional: convertir pruebas fuzz existentes en especificaciones formales para binarios compilados de RISC-V. Claude generó el código de las pruebas, y el núcleo de Rocq lo comprobó frente a esas especificaciones. Theorem aportó las semánticas de las instrucciones RISC-V y de los procesos Linux empleadas en el modelo.
La comprobación de Rocq establece que una prueba se deriva de la especificación formal. La especificación, a su vez, fija qué propiedad se intenta demostrar y bajo qué supuestos; el comprobador no determina si ese modelo recoge todos los comportamientos posibles de un sistema real.
Qué cubren los 239 puntos de entrada
Anthropic informó de pruebas para 239 puntos de entrada seleccionados en 123 bibliotecas OSS-Fuzz. La propiedad principal era que cada punto de entrada no provocara un fallo ante ninguna entrada inferior a 64 MB, según el programa formalizado y sus supuestos. El modelo representaba un binario estático, monohilo, compilado para RISC-V, con un presupuesto fijo de memoria y semántica de Linux. La longitud mediana de los binarios era de 18.000 instrucciones RISC-V.
Un punto de entrada es una función o ruta desde la que se inicia una prueba. Verificar algunos puntos no equivale a cubrir todas las funciones de una biblioteca: Anthropic indicó que no se comprobaron todos sus puntos de entrada. Por eso, el resultado se refiere a esos casos y a la propiedad de ausencia de fallos definida para ellos.
Errores que Claude encontró durante las pruebas
Anthropic también comunicó errores que Claude detectó mientras intentaba completar las pruebas y que el modelo parcheó antes de generar de nuevo la especificación. Un caso afectaba a un descompresor: un subdesbordamiento de contador podía causar una escritura fuera de límites con una disposición poco frecuente de datos de alrededor de 20 MB.
En un decodificador de imágenes, el informe describió una lectura fuera de límites que requería una entrada de 64 MB y más de 2 GB de memoria. Anthropic también informó de un error que dependía de una secuencia concreta de llamadas sobre dos identificadores del mismo archivo, y del redescubrimiento de CVE-2026-56132 en libexpat ante una entrada con anidamiento profundo.
Por qué una prueba formal no certifica una biblioteca completa
La conclusión depende de la especificación, del punto de entrada y de la máquina modelada. Anthropic describió el experimento principal sobre binarios estáticos y monohilo de RISC-V bajo semántica Linux; ese modelo no representa por sí mismo todas las configuraciones de despliegue, como las que usan otras arquitecturas, enlazado dinámico o código que no se alcanza desde los puntos verificados. Quien llama a una biblioteca también puede usarla de maneras que quedan fuera de la propiedad probada.
Las pruebas fuzz y la verificación formal responden a preguntas distintas. El fuzzing ejecuta entradas concretas y puede encontrar fallos en esas ejecuciones. Una prueba formal comprobada puede abarcar todas las entradas representadas por la especificación dentro de sus límites, pero su alcance sigue siendo el del teorema y su modelo. Anthropic señaló además que AddressSanitizer, una herramienta que instrumenta código C y C++ para detectar ciertos errores de memoria durante la ejecución, no detecta todos los problemas de seguridad de memoria.
Qué aclara el apéndice sobre las pruebas y Python
El apéndice de Anthropic distingue alrededor de mil millones de líneas Rocq generadas durante los intentos de unos 180 millones de líneas incluidas en pruebas que pasaron la comprobación. Una prueba completada típica rondaba las 600.000 líneas distribuidas en unos 1.400 archivos; las ejecuciones del comprobador consumían entre 30 minutos y varias horas de tiempo de CPU.
El apéndice también describe un caso separado: Verus comprobó los 17 niveles de un intérprete de Python escrito en Rust frente a la semántica formal del proyecto. La comparación con CPython fue empírica: Anthropic informó de un comportamiento coincidente en el 99,95 % de más de 1,7 millones de programas generados. Esa cifra corresponde a las pruebas realizadas, mientras que el resultado formal se refiere a la semántica especificada para el intérprete.
