Anthropic y su socio Theorem usaron Claude para generar alrededor de 180 millones de líneas de código de demostración matemática en apenas unas semanas, verificadas sobre los programas de prueba de 123 bibliotecas de código abierto del proyecto de seguridad OSS-Fuzz de Google.

Hasta ahora, demostrar formalmente que un programa se ejecuta sin errores era carísimo: el núcleo del sistema operativo seL4 requirió 20 años-persona de especialistas, y el método se reservaba para casos extremos como el software de la aviónica de Airbus.

El método propuesto es radicalmente distinto: en lugar de escribir código nuevo, Claude traduce las pruebas de fallo a problemas matemáticos, analiza el código máquina compilado y produce pruebas formales que un verificador independiente, Rocq, comprueba de forma automática, con muy poca intervención humana. Los investigadores lo llaman generación de pruebas «plenamente autónoma», aunque las herramientas y las bases formales fueron construidas por personas en Theorem.

El resultado más interesante que el titular son los fallos: Claude se topó con cientos de errores y pudo corregirlos él mismo, muchos de ellos invisibles para las pruebas convencionales porque solo se disparan con condiciones muy específicas, como archivos de entrada inusualmente grandes o una secuencia concreta de accesos.

En la verificación de un lector de PDF ampliamente usado, el equipo encontró tantos fallos de seguridad en una semana como los que normalmente se reportan en todo un año para ese software. En otra aplicación, Claude detectó un error lógico que llevaba más de una década sin ser detectado.

Anthropic es cauto en las conclusiones: «verificado formalmente» no significa «sin errores». Las pruebas solo se sostienen bajo condiciones estrictas, como una arquitectura de procesador concreta, programas de un solo hilo y entradas por debajo de 64 MB, mientras que en la práctica esas librerías se ejecutan en hardware y configuraciones diferentes.

El coste computacional es alto: algunas pruebas individuales consumen cientos de millones de tokens y la compañía no publica el coste total del proyecto. Como contrapeso, las pruebas resultó ser reutilizables y los modelos más nuevos son más eficientes: Opus 5.5 resuelve la mitad de las pruebas con alrededor de un 40% menos de tokens que Opus 5.

La hoja de ruta de Theorem ya apunta a infraestructura crítica como glibc, OpenSSL y cURL, con el objetivo declarado de que la verificación formal con IA sea tan rutinaria como las pruebas habituales.

La pregunta que deja abierto el trabajo ya no es si la IA puede programar, sino si puede demostrar que el código que escribe es correcto. Si la respuesta se vuelve rutinaria, la revisión humana del software cambia de naturaleza.

Fuentes

Fuentes
The Decoder — Anthropic's Claude now writes code and proves it safe automatically
Anthropic — Formal verification

Crédito de la imagen: Unsplash — pickawood