| Dato | Cifra |
|---|---|
| Puntos de entrada verificados | 239 |
| Bibliotecas open source (OSS-Fuzz) | 123 |
| Líneas de prueba en Rocq | ~180 millones |
| Límite de entrada por prueba | 64 MB |
| Arquitectura objetivo | RISC-V, binarios de un solo hilo |
| Eficiencia: Opus 5.5 vs Opus 5 | ~40% menos tokens para la mitad de las tareas |
Cifras publicadas por Anthropic el 22 de octubre de 2026.
El experimento
El Frontier Red Team de Anthropic, trabajando con la empresa Theorem, puso a Claude a generar pruebas matemáticas formales de que software existente es correcto. El modelo produjo alrededor de 180 millones de líneas de código de prueba en pocas semanas, a partir de programas de prueba de 123 bibliotecas open source del proyecto de seguridad OSS-Fuzz de Google.
Cómo funciona
En lugar de escribir código nuevo, Claude verifica software existente: traduce pruebas de fallos a problemas matemáticos, analiza el código máquina compilado y produce las demostraciones. Un verificador independiente llamado Rocq comprueba automáticamente esas pruebas, y según Anthropic el proceso casi no necesita revisores humanos.
Bugs reales que las pruebas tradicionales no vieron
Durante la generación de pruebas, Claude encontró cientos de bugs y pudo corregirlos él mismo. Muchos solo aparecen en condiciones muy específicas (archivos de entrada inusualmente grandes o secuencias particulares de accesos). En un lector de PDF muy usado, el equipo encontró en una semana tantos bugs de seguridad como los que se reportan en un año entero; en otra aplicación detectó un error lógico que llevaba más de una década sin descubrirse.
Los límites, sin edulcorantes
Anthropic reconoce que "formalmente verificado" no significa "sin errores": las pruebas solo valen bajo condiciones estrictas (una arquitectura de procesador concreta, programas de un solo hilo, entradas menores de 64 MB). El costo de cómputo es alto: pruebas individuales consumen cientos de millones de tokens. Aun así, los modelos nuevos son más eficientes: Opus 5.5 resuelve la mitad de las pruebas con ~40% menos tokens que Opus 5.
Qué sigue
Si la IA puede verificar su propio código, la pregunta cambia de "¿puede la IA programar?" a "¿puede la IA demostrar que su código es seguro?". Theorem ya apunta a infraestructura crítica como glibc, OpenSSL y cURL.
Anthropic en contexto
Fundada en 2021 por exinvestigadores de OpenAI liderados por Dario y Daniela Amodei, Anthropic desarrolla la familia de modelos Claude con un enfoque declarado en la seguridad de la IA, y ha recibido inversiones multimillonarias de Amazon y Google.
