Qué se demostró exactamente
El equipo rojo de frontera de Anthropic, junto con Theorem, publicó el 22 de octubre los resultados de un intento de usar Claude para verificación formal a gran escala. El equipo tomó pruebas de fuzzing ya existentes de OSS-Fuzz, de Google, trató cada prueba como una propiedad que el código debe satisfacer, la compiló a ensamblador RISC-V y pidió a Claude demostraciones verificables por máquina de que el binario resultante nunca falla.
La propiedad es estrecha y precisa: para cualquier entrada menor de 64 MB, el programa no se caerá con un error de seguridad de memoria ni con una aserción fallida. Las demostraciones suponen un binario estático de un solo hilo con un presupuesto fijo de memoria sobre una CPU RISC-V bajo Linux, y confían en el verificador Rocq, en la semántica de RISC-V y de procesos Linux de Theorem y en el hardware y el compilador de OCaml que hay debajo.
Las cifras
En 123 bibliotecas de código abierto, Claude demostró que 239 puntos de entrada están libres de caídas bajo esa especificación. Las demostraciones suman unos 180 millones de líneas de Rocq. Una típica ocupa unas 600.000 líneas, frente a una longitud mediana del binario de unas 18.000 instrucciones RISC-V. El trabajo llevó unas pocas semanas.
Anthropic no dice cuántos puntos de entrada se intentaron en total, de modo que las cifras no permiten calcular una tasa de éxito. La compañía señala que publica las demostraciones de las pruebas que no necesitaron parche, y las especificaciones de las que no pudo demostrar.
Aparecieron cientos de fallos por el camino, y Claude los parcheó, lo que regeneraba las especificaciones. Entre los ejemplos citados hay un desbordamiento por defecto de un contador en un descompresor que provoca una escritura fuera de límites solo con una disposición rara de unos 20 MB de entrada, una lectura fuera de límites en un descodificador de imagen que exige una entrada de 64 MB y más de 2 GB de memoria, y el redescubrimiento de CVE-2026-56132 en libexpat. Otro era una función de restricción de archivos que no siempre se aplicaba: un fallo lógico que nunca provoca una caída y llevaba latente más de una década.
El atajo evidente y qué hicieron con él
El montaje tiene un agujero que el propio equipo nombra. Claude podía volver demostrable un teorema reescribiendo el programa para que nunca fallara. Anthropic afirma que penalizó los parches que cambiaban el comportamiento, dio crédito adicional por demostrar qué entradas modifica un parche y registró y auditó cada uno.
El problema abierto es el coste
En un banco de 36 tareas pequeñas de verificación construidas con código real de OSS-Fuzz, con tres intentos independientes y cinco millones de tokens de presupuesto cada uno, Opus 5.5 demostró la mitad usando alrededor de un 40% menos de tokens que Opus 5. Los agentes autorizados a copiar las demostraciones de otros desde un espacio compartido usaron un 17% menos de tokens y completaron 34 de las 36, frente a 32 de los que trabajaban solos.
Anthropic es explícita sobre los límites. «Verificado formalmente» no significa libre de errores: un verificador no puede confirmar que la especificación corresponda a la realidad, y pueden quedar fallos en la especificación, en el modelo de máquina o en la base de confianza. Las demostraciones cubren binarios RISC-V enlazados con musl, mientras que la mayoría de los despliegues usan x86 o ARM con glibc enlazado dinámicamente. Y una sola demostración puede costar cientos de millones de tokens, lo que la empresa llama un problema abierto clave.
Aparte, Claude escribió una especificación a partir del RFC 1950 y demostró que la implementación de zlib del núcleo de Linux la cumple a nivel de binario x86. Anthropic afirma haberlo repetido con unas seis bibliotecas más de uso extendido. Si ese trabajo en x86 se generaliza es lo que conviene vigilar.
