Claude escribió demostraciones matemáticas sobre el código compilado de 123 bibliotecas de uso corriente. El resultado: 239 puntos de entrada que resisten cualquier dato de menos de 64 megabytes, bajo condiciones que el propio trabajo declara. Lo hizo el equipo rojo de Anthropic junto con la empresa Theorem, y lo publicó el 22 de octubre. En el camino, el sistema encontró fallas que habían sobrevivido a billones de ejecuciones de pruebas automáticas.
De acuerdo con lo publicado por Anthropic, el trabajo cubre más de un centenar de bibliotecas de código abierto. Todas forman parte de OSS-Fuzz, el banco de pruebas que Google mantiene para buscar fallas en software. Una demostración, en este terreno, es un argumento que una máquina revisa paso a paso hasta comprobar que la conclusión se sigue de las premisas. No afirma que el programa haga lo correcto. Afirma que, en ese modelo del procesador y del sistema operativo, no puede caerse.
El volumen de demostraciones matemáticas explica por qué a esta escala no se había intentado. Claude escribió casi mil millones de líneas y el verificador aceptó unas 180 millones: casi una de cada cinco. Una prueba típica ronda las 600.000 líneas para un programa de 18.000 instrucciones. Cada una vuelve a probar desde cero el arranque, el gestor de memoria y la biblioteca estándar.
Cómo se prueba que un programa no puede caerse
El punto de partida es una prueba automática de las que ya existen. Un programa recibe entradas al azar y busca una que lo tumbe. Claude tradujo esa prueba a una especificación formal. La aplicó al binario compilado para procesadores RISC-V, el último eslabón antes de que el programa corra. Escribió la demostración en Rocq, un lenguaje con reglas que una máquina revisa paso a paso. Esa máquina la aceptó.
La garantía descansa en tres piezas: los modelos formales del procesador y del sistema operativo, la afirmación que se quiso probar y el verificador. El resto no necesita revisión humana. Por eso el enfoque escala: se pueden sumar proyectos sin agrandar la parte que hay que creer.
El equipo también comparó el alcance de una prueba con el de una demostración. Construyó un intérprete de Python en Rust, con 17 niveles verificados uno por uno, y le inyectó siete errores a propósito. Las pruebas aleatorias detectaron dos. La demostración falló con los siete.
Por qué las demostraciones matemáticas no cierran el problema
El alcance es estrecho y el texto lo dice. Los binarios son de un solo hilo, con memoria fija, en RISC-V con Linux y enlazados de forma estática. La mayoría de esas bibliotecas se ejecuta en procesadores x86 o ARM, con enlace dinámico. La propia Anthropic escribe que «verificado» no significa «sin errores». El verificador no puede saber si la especificación describe la realidad. El uso indebido por parte de quien llama queda fuera.
Hay un riesgo adicional que el equipo reconoce. Un modelo podría hacer demostrable una afirmación reescribiendo el código para que nunca falle, en vez de arreglar el problema. Para evitarlo penalizaron los parches y auditaron cada uno.
También pesa quién firma. El trabajo es de Anthropic sobre sus propios modelos, sin revisión independiente todavía. Cubre 239 puntos de entrada, no todas las funciones de cada biblioteca. Theorem ofrece correr el mismo proceso en otros proyectos y publica una guía para que un equipo lo intente con su propio código.
La consecuencia práctica es un cambio de costo. Encontrar fallas se volvió barato; demostrar que un programa no las tiene empieza a serlo también. Lo que sigue sin automatizarse es decidir qué significa que un programa esté bien, y esa definición la escriben personas.
Otras fuentes consultadas: Anthropic, apéndice técnico (22/10/2026); The Injection (22/10/2026); AI Weekly (23/10/2026). (Resultados reportados por Anthropic y Theorem, sin revisión independiente.)
