Claude escribe código y demuestra matemáticamente que es seguro, según Anthropic y Theorem

Anthropic ha utilizado a Claude para demostrar matemáticamente que código ya existente es correcto. Según el artículo de The Decoder, el enfoque ataca un problema central del software generado por IA, aunque tiene límites prácticos estrictos.

Hasta ahora, demostrar que un programa funciona sin errores en todas las circunstancias resultaba prohibitivamente caro. Un equipo de especialistas necesitó 20 años-persona para verificar formalmente seL4, un núcleo de sistema operativo pequeño, de modo que el método se reservaba para casos extremos como el software de aviónica de Airbus.

El Frontier Red Team de Anthropic, junto con su socio Theorem, dejó que Claude asumiera el trabajo de las demostraciones. El modelo produjo unos 180 millones de líneas de código de prueba matemática en pocas semanas, a partir de programas de prueba de 123 bibliotecas de código abierto del proyecto de seguridad OSS-Fuzz de Google.

Claude no escribió código nuevo, sino que verificó software existente: tradujo pruebas de fallos a problemas matemáticos, analizó el código máquina compilado y generó extensas demostraciones. Un programa de verificación independiente, Rocq, comprueba automáticamente esas pruebas y, según Anthropic, el proceso apenas requiere revisores humanos. Los investigadores lo describen como generación de pruebas «totalmente autónoma», aunque las herramientas y los fundamentos formales los construyeron personas de Theorem.

Durante el proceso, Claude encontró cientos de errores y se le permitió corregirlos. Muchos habrían pasado desapercibidos en pruebas convencionales porque solo aparecen en condiciones muy concretas, como archivos de entrada inusualmente grandes o una secuencia particular de accesos. En el intento de verificar un lector de PDF muy usado, el equipo halló en una semana tantos errores de seguridad como los que suelen notificarse para ese software en un año entero. En otra aplicación, Claude detectó un error lógico que llevaba más de una década sin descubrirse. Anthropic señala que, aunque una demostración completa acabe fallando, el intento igualmente saca a la luz fallos reales.

Anthropic reconoce que «verificado formalmente» no equivale a «libre de errores». Las pruebas solo valen bajo condiciones estrictas: una arquitectura de procesador concreta, programas de un solo hilo y entradas de menos de 64 MB. En la práctica, estas bibliotecas se ejecutan en otro hardware y con otras configuraciones. El coste de cómputo también es elevado: cada demostración puede consumir cientos de millones de tokens, y Anthropic no informa del coste total del proyecto.

Una prueba más pequeña mostró que las demostraciones son reutilizables y que los modelos nuevos son más eficientes: según el artículo, Opus 5.5 resuelve la mitad de las pruebas con aproximadamente un 40 % menos de tokens que Opus 5.

La lectura de fondo es que, si la IA puede verificar su propio código, los desarrolladores podrían confiar más en el software generado por IA y dedicar menos tiempo a revisarlo. La pregunta pasaría de «¿puede la IA programar?» a «¿puede la IA demostrar que el código que escribe es seguro?». Anthropic espera que la verificación formal con IA llegue a ser tan práctica como las pruebas estándar, y la hoja de ruta de Theorem ya apunta a infraestructura crítica como glibc, OpenSSL y cURL.

Nota: el texto descargado es el artículo completo de The Decoder, que se basa en el anuncio de Anthropic; las cifras citadas son las que publica ese medio.