✨︎ Resumen (TL;DR):
- Anthropic anunció que Claude generó demostraciones para 239 puntos de entrada de 123 bibliotecas de código abierto con Theorem.
- El repositorio público reúne 60 puntos de entrada de 25 bibliotecas; el apéndice reporta unos 180 millones de líneas de Rocq en las demostraciones aceptadas.
- Las garantías se limitan al código alcanzable y a binarios estáticos de RISC-V, con entradas de menos de 64 MiB.
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. La empresa reportó cientos de errores y resultados que descartan fallos concretos bajo condiciones definidas; la primera entrega pública deja revisar 60 puntos de entrada de 25 bibliotecas con sus enunciados y binarios.
La verificación formal es un proceso matemático que comprueba que un programa cumple propiedades definidas para todas las entradas admitidas, dentro de un modelo específico. Para este trabajo, Claude escribió las demostraciones y Rocq comprobó que cumplían los enunciados. Esa comprobación lógica ocurre fuera del modelo de IA.
De las pruebas de OSS-Fuzz a las demostraciones
El flujo 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 verificó que satisfacían los enunciados.
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.
Un fallo de memoria y una prueba de gran tamaño
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. Por eso, cada demostración debe vincularse con la versión que se verificó.
Las demostraciones aceptadas sumaron unos 180 millones de líneas de Rocq, según el apéndice técnico. Una prueba típica rondó las 600,000 líneas, porque también debía cubrir rutinas de arranque y componentes de soporte.
Qué cubren las garantías de Theorem
El repositorio limita sus resultados al código alcanzable desde cada punto de entrada y a binarios estáticos de RISC-V. Quedan fuera errores que los detectores no identifican, como ciertos resultados incorrectos o las fugas de memoria.
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 con un solo hilo y memoria limitada. La validez depende del modelo, de los enunciados y de Rocq.
El repositorio permite revisar una parte
El repositorio público de Theorem reúne pruebas para 60 puntos de entrada de 25 bibliotecas, junto con los enunciados y los binarios correspondientes. Es una parte del resultado anunciado por Anthropic, que abarcó 239 puntos de entrada de 123 bibliotecas.
Para reutilizar estos resultados, los desarrolladores cuentan con las versiones y los binarios identificados en el repositorio. Esos datos les permiten contrastar qué demostración corresponde a una compilación concreta.
Las demostraciones, por tanto, son concretas: dependen del código alcanzable, del binario estático de RISC-V, de las entradas admitidas y del entorno de Linux descrito para Theorem.
