Anthropic afirma que Claude demostró propiedades de seguridad en 123 bibliotecas

El 22 de octubre de 2026, Anthropic publicó una investigación en la que informó que, en colaboración con Theorem, Claude produjo pruebas formales verificadas por máquina de propiedades de seguridad a nivel de código ensamblador RISC-V para 239 puntos de entrada de pruebas de fuzzing en 123 bibliotecas de código abierto.

Según Anthropic, Claude corrigió los errores que encontró y luego demostró que los programas siempre finalizarán normalmente, sin provocar errores de seguridad de memoria ni fallos en aserciones, para cualquier entrada inferior a 64 MB y cualquier respuesta del sistema operativo Linux y disposición de memoria incluidos en el modelo. Las pruebas suponen que el programa se ejecuta como un binario estático de un solo hilo, con un presupuesto de memoria fijo, en una CPU RISC-V que usa Linux. Anthropic dijo que las pruebas constan de unos 180 millones de líneas de Rocq y que una prueba típica tiene unas 600.000 líneas para cubrir binarios con una longitud mediana de 18.000 instrucciones RISC-V. La empresa afirmó que, hasta donde sabe, este es el primer esfuerzo a gran escala por utilizar IA para aplicar verificación formal a software de producción a nivel de código ensamblador.

Se está publicando en GitHub una parte de las pruebas, junto con la semántica de RISC-V y del sistema operativo que las sustenta. Anthropic dijo que también está publicando los componentes de confianza creados para el proyecto que aún no eran públicos, pruebas completas de las pruebas de fuzzing que no requirieron correcciones y especificaciones de las pruebas de fuzzing que no pudo demostrar, aunque no divulgará las pruebas que podrían revelar un error sin corregir.

Convertir pruebas de fuzzing en pruebas formales

El método convierte la prueba de fuzzing existente y compilable de cada biblioteca en una especificación formal que codifica una regla: la prueba nunca se bloquea con ninguna entrada inferior a 64 MB. La especificación se define sobre instrucciones RISC-V compiladas, mediante la semántica formal de Theorem para el conjunto de instrucciones RISC-V y los procesos de Linux, y el comprobador de pruebas de Rocq verifica cada prueba terminada con respecto a la especificación. Anthropic afirma que, con este método, los desarrolladores solo tienen que confiar en tres componentes: los modelos formales de RISC-V y de los procesos de Linux, los enunciados exactos de los teoremas y el propio comprobador de Rocq.

Anthropic dijo que aplicó este proceso a cientos de proyectos de la iniciativa OSS-Fuzz de Google, que ofrece pruebas de fuzzing continuas para proyectos de código abierto que cumplen los requisitos e instrumenta automáticamente programas C y C++ con AddressSanitizer, una herramienta que bloquea un programa cada vez que se accede a la memoria de forma incorrecta. Un apéndice fechado el 22 de octubre de 2026 detalla el teorema completo demostrado: para todas las entradas inferiores a 64 MiB y todas las disposiciones de memoria, ni el binario instrumentado con ASan ni el binario sin instrumentar provoca un fallo, se interrumpe ni presenta un comportamiento no incluido en el modelo; además, ambos producen trazas de lectura y escritura, comportamiento de salida y estado final del sistema de archivos idénticos.

El apéndice señala que Claude escribió alrededor de mil millones de líneas de Rocq durante el proyecto, de las cuales unas 180 millones superaron la comprobación de pruebas. El punto de entrada del analizador de 391 líneas de cJSON recibió una prueba de 630.000 líneas, mientras que fftw3, con 51.000 líneas enlazadas, recibió una prueba de 480.000 líneas. Como se permitió que Claude corrigiera el código antes de completar una prueba, Anthropic dijo que penalizó las correcciones, ofreció puntos adicionales por demostrar qué entradas modificaba cada corrección y registró y auditó las correcciones para desalentar la manipulación de las recompensas.

Errores descubiertos durante los intentos de demostración

Anthropic informa que los intentos de demostrar las propiedades sacaron a la luz cientos de errores, muchos de los cuales probablemente un fuzzer no habría encontrado. Mientras demostraba un punto de entrada de una biblioteca, Claude encontró un desbordamiento por defecto de un contador en un descompresor que provocaba una escritura fuera de los límites, pero solo con entradas de unos 20 MB que presentaban una disposición específica y poco común. Entre los demás hallazgos hubo una lectura fuera de los límites en un decodificador de imágenes que requería una entrada de 64 MB y más de 2 GB de memoria; otra lectura fuera de los límites que requería una secuencia determinada de llamadas a través de dos identificadores del mismo archivo; y el redescubrimiento de CVE-2026-56132 en libexpat, que requería una entrada profundamente anidada.

Claude también encontró errores lógicos que nunca provocan un bloqueo, incluida una restricción sobre los archivos que puede cargar una aplicación que no siempre se aplica. Anthropic dijo que los intentos de verificación de varias aplicaciones críticas de uso generalizado revelaron un error lógico hasta entonces desconocido, que había permanecido latente durante más de una década. También indicó que, durante un esfuerzo por verificar un lector de PDF de uso generalizado, encontró en una semana tantos errores de seguridad como los que suelen notificarse en un año.

Experimentos adicionales y hallazgos sobre eficiencia

Además de OSS-Fuzz, Anthropic pidió a Claude que redactara una especificación formal de RFC 1950, el documento técnico que define el formato de compresión zlib, y luego demostrara que la implementación de zlib del núcleo de Linux lo implementa correctamente. Claude demostró directamente el binario compilado para x86 mediante una semántica formal del conjunto de instrucciones x86 generada por Claude. Anthropic dijo que repitió el proceso con media docena de otras bibliotecas de uso generalizado y encontró errores menores en casos límite que no podían explotarse y que se están notificando a los responsables de los proyectos. La empresa también informó que, al generar la semántica de x86, se identificaron cientos de errores en la documentación oficial de referencia y una cantidad menor de errores en el propio hardware; además, la ejecución paso a paso de la semántica puede iniciar un espacio de usuario de Ubuntu en un núcleo de Linux.

En otro experimento, Claude creó en Rust un intérprete para un amplio subconjunto de Python y demostró, mediante la herramienta de verificación Verus, que se ajusta a la semántica de CPython descrita en un artículo académico. El apéndice técnico afirma que se demostró la corrección de los 17 niveles del intérprete, con el teorema de que «Siempre que el intérprete devuelve un resultado, ese resultado es el que prescribe la semántica formal». Anthropic afirmó que las pruebas empíricas con 1,7 millones de programas de Python generados aleatoriamente encontraron un comportamiento idéntico al de CPython en el 99,95 % de los casos; de siete errores introducidos deliberadamente, cinco superaron las pruebas aleatorias, mientras que los siete hicieron fallar la demostración formal.

Para medir la eficiencia, Anthropic creó 36 pequeñas tareas de verificación a partir de puntos de entrada reales de OSS-Fuzz, reducidos para generar programas de entre 283 y 2.491 instrucciones, con entradas limitadas a 64 bytes y AddressSanitizer sustituido por un entorno de ejecución «mini-ASan» de unas 100 instrucciones. Anthropic informa que Opus 5.5 demuestra la mitad de las tareas con aproximadamente un 40 % menos de tokens que Opus 5. Anthropic también informa que los agentes a los que se permitió copiar las demostraciones de los demás en un espacio de trabajo compartido necesitaron un 17 % menos de tokens que los agentes que trabajaron solos; algunos lograron completar las tareas después de haber fracasado previamente por su cuenta, y los agentes que trabajaron solos no consiguieron completar dos de las demostraciones. La empresa afirmó que el mismo efecto de reutilización se observó a gran escala durante el trabajo con OSS-Fuzz, cuando equipos de agentes copiaron demostraciones terminadas y las adaptaron, ya que gran parte de cada demostración abarca código compartido de inicialización del entorno de ejecución de C y de AddressSanitizer.

Limitaciones declaradas y programa OSS Verify

Anthropic afirma que las demostraciones no significan que las bibliotecas estén libres de errores: los errores restantes podrían estar en los componentes de confianza o fuera del alcance de las demostraciones. Estas abarcan binarios estáticos RISC-V de un solo hilo enlazados con musl libc, mientras que la mayoría de los usuarios ejecuta estas bibliotecas en x86 o ARM y las enlaza dinámicamente con glibc; además, AddressSanitizer no detecta todos los errores de seguridad de memoria. La empresa dijo que espera que estas limitaciones se vuelvan manejables a medida que mejoren los modelos.

Theorem ofrece gratis el mismo flujo de trabajo a proyectos de código abierto que cumplan los requisitos, a través de su programa OSS Verify. La inscripción se realiza mediante una solicitud de incorporación de cambios que añade los archivos project.yaml, Dockerfile y build.sh al repositorio del programa; Theorem afirma que evalúa los proyectos siguiendo criterios similares a los de OSS-Fuzz y da prioridad a la infraestructura crítica de uso extendido. Según Theorem, los responsables de mantenimiento reciben una demostración Rocq, verificada por el núcleo de Rocq, de que cada objetivo de fuzzing no se bloquea con ninguna entrada de hasta 64 MiB; los errores encontrados durante el proceso de demostración se comunican de forma privada a los responsables de mantenimiento por correo electrónico, sin plazo para hacerlos públicos, y las demostraciones pueden tardar varios días en producirse. La hoja de ruta de Theorem tiene como objetivo verificar todo el ecosistema Nix, incluida infraestructura crítica como glibc, OpenSSL y cURL.