La verificación formal, demostrar matemáticamente que un código se comporta como se especifica, es desde hace tiempo el patrón oro de la seguridad y demasiado cara para casi todos. Anthropic da una referencia elocuente: el núcleo seL4 costó dos años-persona escribirlo y 20 verificarlo. En colaboración con la empresa de verificación Theorem, Anthropic informa ahora de que Claude produjo esas demostraciones a una escala impensable hace pocos años.
El truco fue evitar escribir especificaciones a mano. El equipo tomó pruebas de fuzzing del programa OSS-Fuzz de Google, pequeños puntos de entrada en los que cualquier fallo cuenta como error, y convirtió cada una en una afirmación formal: el binario RISC-V compilado nunca falla, incluidos los errores de seguridad de memoria que detecta AddressSanitizer, con ninguna entrada de menos de 64 MB. En unas pocas semanas, Claude lo demostró para 239 puntos de entrada en 123 bibliotecas, corrigiendo por el camino los errores que encontró. Las demostraciones, sobre todo en el asistente de pruebas Rocq, suman unos 180 millones de líneas, con una demostración típica de unas 600.000 líneas para un binario con una mediana de 18.000 instrucciones. Nadie necesita leerlas; el verificador de Rocq las confirma.
Los errores son el beneficio inmediato. Varios eran de los que un fuzzer rara vez encuentra, como una escritura fuera de límites en un descompresor que solo aparecía con entradas de unos 20 MB con una disposición concreta. Otros experimentos demostraron el zlib del núcleo Linux frente a una versión formal de RFC 1950 y comprobaron un intérprete en Rust para un subconjunto de Python, que coincidió con CPython en el 99,95% de 1,7 millones de programas aleatorios. El coste también baja: en 36 tareas pequeñas, Claude Opus 5.5 demostró la mitad con un 40% menos de tokens que Opus 5, y compartir demostraciones entre agentes ahorró un 17%.
Para quienes mantienen bibliotecas, es la prueba más sólida hasta ahora de que las garantías verificadas por máquina podrían volverse rutinarias, como lo hizo el fuzzing. Theorem se ofrece a ejecutar el proceso para otros proyectos de código abierto y ha publicado una skill de Claude.
Los autores son cuidadosos con los límites, y los lectores deberían serlo también. Verificado no es lo mismo que libre de errores. Las demostraciones cubren compilaciones RISC-V de un solo hilo, enlazadas estáticamente con musl, mientras que la mayoría de usuarios ejecuta estas bibliotecas en x86 o ARM con glibc. AddressSanitizer no detecta todos los errores de memoria, no se cubrieron todos los puntos de entrada y quien llama a una biblioteca aún puede usarla mal. Las demostraciones pueden costar además cientos de millones de tokens, y esa es la verdadera barrera para hacerlo con todo el ecosistema.