Anthropic anunció el 22 de octubre de 2026 que Claude generó demostraciones matemáticas para 239 puntos de entrada de 123 bibliotecas de código abierto, con Theorem. El trabajo encontró cientos de errores y descarta fallos concretos bajo condiciones definidas, según la empresa.
La entrega pública inicial permite examinar una parte del resultado. El repositorio de Theorem reúne pruebas para 60 puntos de entrada de 25 bibliotecas, con los enunciados y los binarios a los que corresponden.
De las pruebas con ejemplos a las demostraciones
El proyecto partió de pruebas existentes de OSS-Fuzz, la iniciativa de Google que busca errores mediante numerosos datos de entrada. Un punto de entrada es una vía preparada por los desarrolladores para probar una parte del código.
El flujo convirtió esas pruebas en propiedades que debían cumplirse para todas las entradas admitidas. Claude escribió demostraciones sobre programas compilados para RISC-V, una arquitectura de procesadores, y Rocq comprobó que satisfacían los enunciados. Esa comprobación lógica es externa al modelo de IA.
El apéndice técnico fija el límite en entradas de menos de 64 MiB. También describe la comparación entre versiones con y sin AddressSanitizer, una herramienta que detecta errores de memoria, para establecer que la instrumentación conserva el comportamiento observable del programa.
Entre los hallazgos, Anthropic describe un contador que descendía por debajo de su mínimo y provocaba una escritura fuera de límites en un descompresor. El fallo requería una entrada de unos 20 MB con una disposición poco habitual. Cuando Claude modificaba el código para corregir un error, la prueba posterior correspondía a esa versión modificada.
Las demostraciones aceptadas sumaron unos 180 millones de líneas de Rocq, según el apéndice. Una prueba típica rondó las 600,000 líneas, porque también debía cubrir rutinas de arranque y componentes de soporte.
Las garantías dependen del código y del entorno
El repositorio limita sus resultados al código alcanzable desde cada punto de entrada y a binarios estáticos de RISC-V. Errores que los detectores no identifican, como ciertos resultados incorrectos o fugas de memoria, quedan fuera de su alcance.
También establece una distinción relevante: ninguna prueba de esta entrega pública descarta ejecuciones que nunca terminan. Demostrar que no aparece un fallo cubierto por el enunciado deja abierta la posibilidad de que el programa siga ejecutándose indefinidamente.
La documentación del modelo de Theorem describe un proceso de Linux de un solo hilo, con memoria limitada. La validez depende del modelo, los enunciados y Rocq.
Para reutilizar estos resultados, los desarrolladores cuentan con versiones y binarios identificados en el repositorio. Esos datos permiten contrastar qué demostración corresponde a una compilación concreta.
