📻 Versión en audio: si prefieres escuchar en vez de leer, el resumen del artículo está justo aquí arriba.
La IA dejó de cazar bugs y ahora demuestra matemáticamente que no existen
Cada vez que un fuzzer encuentra un bug, la pregunta incómoda sigue en pie: ¿cuántos quedan? La respuesta honesta es no se sabe, y tu fuzzer jamás va a terminar de buscar. El fuzzing es adivinación a la fuerza: millones de entradas mutadas contra una puerta de entrada, esperando que algo reviente. Por mucho que corra, nunca puede garantizar que agotó todos los caminos. Esa incomodidad es justo la que atacó Anthropic junto a la startup Theorem, y el resultado me parece el anuncio más interesante de la semana en seguridad.
180 millones de líneas de prueba
Usaron Claude para escribir pruebas formales de que un programa no crashea, y las verificaron a nivel de assembly: 239 puntos de entrada de 123 librerías open source que forman parte del OSS-Fuzz de Google, el programa de fuzzing continuo más riguroso del ecosistema. Todo eso compila a binarios RISC-V y las pruebas, escritas en Rocq (un verificador de teoremas), suman unos 180 millones de líneas: una prueba típica ronda las 600.000 líneas para garantizar que un binario de 18.000 instrucciones no cae en memory corruption ni en assertion fallida con cualquier entrada de menos de 64 MB.
Ese «cualquier entrada» es la revolución silenciosa. Los fuzzers típicos cortan las mutaciones en 1 MB, así que los bugs que solo aparecen con inputs grandes y un layout puntual estaban fuera del alcance de la fuerza bruta por diseño. La prueba matemática los busca igual, porque no ejecuta: razona sobre todas las rutas posibles de una sola vez.
Los bugs que el fuzzing nunca iba a pillar
De propina, el proceso encontró cosas que un fuzzer difícilmente habría visto: un underflow de contador que derivaba en una escritura fuera de límites, pero solo con entradas de unos 20 MB y un layout específico; un out-of-bounds read en un decodificador de imágenes que pedía 64 MB de entrada y más de 2 GB de memoria; y el redescubrimiento del CVE-2026-56132 en libexpat, escondido tras entradas profundamente anidadas. También bugs lógicos que ni siquiera crashean, uno de ellos latente por más de una década. Y en un lector de PDF muy usado, dijeron haber encontrado en una semana tantos bugs de seguridad como los que normalmente se reportan en un año entero.
Cómo funciona la confianza
El truco está en convertir los tests existentes en una especificación formal: «esta suite de tests nunca puede fallar, para ninguna entrada». Claude escribe la prueba, pero no hay que leerla: el kernel de Rocq la verifica mecánicamente. La base de confianza se contrae a tres piezas — la semántica formal de RISC-V y Linux, el enunciado exacto del teorema y el verificador Rocq — y todo lo demás queda demostrado encima. Ojo con el detalle humano de siempre: también tuvieron que penalizar el reward hacking, porque el modelo a veces prefería parchear el código para que «no crashee» en trivial, en vez de demostrarlo. Como estudiante que cambia el examen en vez de estudiar.
Mi lectura: «formalmente verificado» aún no significa «impecable». Las pruebas asumen binarios estáticos, single-threaded, con musl libc sobre RISC-V; tus servidores corren glibc dinámico sobre x86, así que la brecha existe. Pongámosla en perspectiva con el caso clásico: al kernel seL4 le tomaron dos años-persona implementarlo y veinte verificarlo formalmente. Esa brecha de diez veces es exactamente la que se está cerrando con IA, y se está cerrando rápido.
A mí me toca vivir del otro lado: cada CVE que me obliga a actualizar PHP en la flota un martes en la noche me recuerda que «muy testeado» no significa nada contra un input que nadie imaginó. Un mundo donde el pipeline demuestra que una clase entera de bugs es imposible — no que sobrevivió a dos millones de lanzamientos al azar — cambia la pega de raíz. No es que la máquina encuentre más bugs; es que por primera vez puede certificar su ausencia, y eso es un terreno donde ni el mejor QA humano llega.
Fuente de inspiración: LLMs are making formal software verification feasible at a much larger scale — Anthropic
