Anthropic usó Claude para demostrar matemáticamente que un código ya existente es correcto, informó The Decoder el 23 de octubre de 2026. El método ataca uno de los problemas centrales del software generado con IA, aunque funciona con límites prácticos estrictos.

Demostrar que un programa corre sin errores en cualquier circunstancia siempre fue carísimo. Un equipo de especialistas necesitó 20 años-persona solo para verificar formalmente seL4, un núcleo de sistema operativo pequeño. Por eso la técnica quedaba reservada a casos extremos, como el software de aviónica de Airbus.

El Frontier Red Team de Anthropic, junto a su socio Theorem, le pasó ese trabajo de demostración a Claude. En pocas semanas el modelo produjo cerca de 180 millones de líneas de código de pruebas matemáticas, a partir de los programas de prueba de 123 bibliotecas de código abierto incluidas en OSS-Fuzz, el proyecto de seguridad de Google.

¿Cómo verificó Claude el código?

Claude no escribió código nuevo. Verificó software existente traduciendo pruebas de fallo (crash tests) a problemas matemáticos, analizando el código máquina compilado y generando demostraciones extensas. Un programa de verificación independiente llamado Rocq revisa esas demostraciones de forma automática, y según Anthropic el proceso casi no necesita revisores humanos.

Los investigadores lo llaman generación de pruebas "totalmente autónoma". Las herramientas y los fundamentos formales, eso sí, los construyeron personas en Theorem.

Errores que años de pruebas no vieron

Mientras generaba las demostraciones, Claude se topó con cientos de errores y tuvo permiso para corregirlos. Según los investigadores, muchos habrían pasado inadvertidos en las pruebas convencionales porque solo aparecen en condiciones muy específicas, como archivos de entrada inusualmente grandes o una secuencia particular de accesos.

Al verificar un lector de PDF de uso masivo, por ejemplo, el equipo encontró en una semana tantos errores de seguridad como los que se reportan para ese programa en un año entero. En otra aplicación, Claude detectó un error lógico que llevaba más de una década sin ser descubierto. Anthropic sostiene que incluso cuando una demostración completa termina fallando, el intento igual deja a la vista errores reales.

¿Qué garantiza y qué no la verificación formal?

Anthropic reconoce que "verificado formalmente" no significa "libre de errores". Las demostraciones valen solo bajo condiciones estrictas.

  • Una arquitectura de procesador específica.
  • Programas de un solo hilo.
  • Entradas de menos de 64 MB.

En la práctica, esas bibliotecas corren en hardware distinto y con otras configuraciones.

El costo de cómputo es alto. Algunas demostraciones individuales consumieron cientos de millones de tokens, y Anthropic no informa el costo total del proyecto. El argumento de la empresa es que si la IA puede verificar su propio código, los desarrolladores pueden confiar más en el software generado con IA y dedicar menos tiempo a revisarlo, lo que abarata todo el proceso de programación y no solo la verificación.

Una prueba más acotada mostró además que las demostraciones se pueden reutilizar y que los modelos nuevos son más eficientes. Opus 5.5 resuelve la mitad de las demostraciones con cerca de 40% menos tokens que Opus 5.

Lo que viene

Para The Decoder, si la IA puede escribir código y garantizar que es correcto bajo condiciones definidas, la pregunta deja de ser si la IA sabe programar y pasa a ser si puede demostrar que lo que escribe es seguro.

Anthropic espera que la verificación formal con IA pronto sea tan práctica como las pruebas habituales. La hoja de ruta de Theorem ya apunta a infraestructura crítica como glibc, OpenSSL y cURL.