Verificación formal con IA: siete gates para confiar en una prueba

El 22 de octubre de 2026, cuatro días antes de esta publicación en America/Lima, Anthropic describió una colaboración con Theorem para llevar verificación formal a binarios reales. El experimento convirtió targets existentes de OSS-Fuzz en proposiciones sobre programas RISC-V: bajo un modelo concreto de Linux, un presupuesto de memoria y entradas menores de 64 MB, el ejecutable instrumentado no debe alcanzar errores y debe conservar el comportamiento observable del binario sin sanitizer. Claude produjo las pruebas y el kernel de Rocq las comprobó. El reporte agregado cubre 239 puntos de entrada en 123 bibliotecas y cerca de 180 millones de líneas de prueba.

Ese resultado cambia el cuello de botella, pero no elimina el trabajo humano. Antes, redactar cientos de miles de líneas de prueba por objetivo hacía inviable aplicar métodos formales a software común. Un agente puede explorar ese espacio a escala; el equipo todavía debe decidir qué propiedad importa, revisar el enunciado, fijar el entorno y aceptar la base de confianza. La salida útil no es un texto persuasivo del modelo, sino una cadena reproducible entre binario, especificación, prueba y checker.

El fuzzing busca contraejemplos: ejecuta muchas entradas y celebra cuando encuentra una que rompe una propiedad. Es indispensable, pero una campaña finita no puede recorrer un espacio infinito. El flujo publicado reutiliza el target como especificación ejecutable. Compila una versión normal y otras con AddressSanitizer o UndefinedBehaviorSanitizer, transforma los binarios y su entorno en definiciones formales, y enuncia que ambas ejecuciones concuerdan para toda entrada cubierta. Si el harness llama a abort ante una violación, demostrar que ese error es inalcanzable también demuestra la propiedad codificada por el harness.

El agente intenta construir una prueba en Rocq. Si descubre que el enunciado es falso, puede exponer un bug o proponer un parche; luego el binario, el enunciado y la prueba deben regenerarse. Si completa la prueba, Rocq no confía en la reputación del modelo: comprueba cada paso contra reglas pequeñas. El repositorio público fija versiones del checker, del modelo de proceso Linux, de los binarios y de sus hashes, y ofrece comandos de verificación sin red. Esa independencia es la diferencia entre una respuesta del LLM y evidencia formal.

La publicación agregada y el release público no son idénticos. Al consultarlo el 26 de octubre, el README público enumeraba 60 puntos de entrada con pruebas en 25 bibliotecas, mientras que Anthropic reportaba el esfuerzo completo sobre 239 puntos de entrada y 123 bibliotecas. La diferencia es importante: una afirmación de investigación puede incluir artefactos retenidos por bugs sin parchear o material aún no publicado. Un comprador técnico debe auditar lo disponible, no asumir que todo el resultado anunciado es reproducible hoy.

Imagina una empresa que recibe webhooks firmados de pagos y mantiene un parser nativo para alto volumen. El ejemplo es hipotético. El riesgo elegido no es probar que todo pago se contabiliza correctamente; eso mezcla red, reloj, reintentos y reglas contables. El piloto comienza con una propiedad estrecha: para todo payload de hasta cierto tamaño que entra por el harness, el parser no accede memoria fuera de límites y la versión instrumentada conserva las mismas salidas observables que el binario normal dentro del modelo aceptado.

El equipo fija el commit, compilador, flags, dependencias y arquitectura. Seguridad revisa el enunciado; ingeniería mantiene tests y fuzzing para encontrar fallos fuera del alcance formal; una pipeline separada vuelve a comprobar la prueba en un checker fijado por digest. Si el agente propone cambiar el parser para que el teorema sea demostrable, el parche entra por revisión ordinaria y el equipo exige una prueba de equivalencia o documenta la diferencia. La prueba se adjunta al release como evidencia de esa propiedad, no como certificado global del servicio.

Primero, el enunciado debe nombrar una propiedad que el negocio entiende: seguridad de memoria, round-trip, equivalencia o una invariante concreta. Segundo, el alcance debe fijar entrada, límites, arquitectura, sistema operativo, memoria, concurrencia y comportamiento observable. Tercero, la procedencia debe enlazar commit, dependencias, compilador, flags, binarios y hashes; una prueba sobre otros bytes no cubre el release. Cuarto, la base de confianza debe quedar explícita: kernel del checker, axiomas permitidos, modelo de máquina y herramientas que convierten el ejecutable en una representación formal.

Quinto, la comprobación debe ser independiente del agente y fallar cerrada en CI si cambia un artefacto, aparece un axioma no permitido o la prueba deja de compilar. Sexto, bug, parche y prueba son entregables separados: un modelo puede hacer trivial el teorema modificando funcionalidad, por lo que cada cambio necesita revisión y, cuando corresponde, equivalencia conductual. Séptimo, la garantía debe mapearse al despliegue real y conservar una etiqueta de alcance visible. Si producción usa x86 dinámico, múltiples hilos y glibc, una prueba sobre un binario RISC-V estático y monohilo es investigación útil, no todavía una aprobación de release.

El piloto debe empezar con uno o dos componentes de riesgo alto y frontera pequeña: parsers, decodificadores, criptografía auxiliar o transformaciones con una ley algebraica clara. Conserva la línea base de tests, sanitizer y fuzzing; la verificación no los reemplaza porque buscan clases distintas de fallo. Registra cuántos targets se formalizaron, cuánto tardó cada intento, qué consumo tuvo, cuántos enunciados terminaron demostrados, qué contraejemplos aparecieron y cuántos hallazgos sobrevivieron la revisión humana. No extrapoles el resultado a toda la biblioteca.

La comparación más útil no es agente contra humano en abstracto. Compara tres decisiones: seguir solo con pruebas dinámicas; añadir intentos formales en componentes seleccionados; o exigir una prueba como gate de ciertos releases. Mide tiempo hasta evidencia, coste por propiedad aceptada, mantenimiento cuando cambia el código, cobertura del binario desplegado y reducción del riesgo que sí importa. Un intento que no produce prueba puede seguir siendo valioso si descubre un bug reproducible; una prueba barata puede ser inútil si el enunciado no representa el riesgo operativo.

El riesgo principal es la brecha entre modelo y realidad. El propio repositorio advierte que su semántica de proceso Linux es incompleta y que las pruebas publicadas hablan de binarios RISC-V estáticos, no del código fuente ni de builds x86-64. Los sanitizer no detectan todos los fallos; un target cubre lo alcanzable desde ese punto de entrada, no toda la biblioteca; y los enunciados de acuerdo publicados no prueban que la ejecución termine. Concurrencia, enlaces dinámicos, hardware, syscalls no modeladas y uso incorrecto por el caller pueden quedar fuera.

También existe riesgo de automatización. Un agente optimizado para cerrar la prueba puede reducir funcionalidad, debilitar el harness o explotar un enunciado vacío. Anthropic reconoce esa posibilidad de reward hacking y describe penalizaciones y auditoría de parches; un equipo de producto debe añadir separación de funciones y pruebas de mutación que demuestren que el harness falla cuando la propiedad se rompe. Finalmente, los artefactos no publicados no deben convertirse en una insignia de marketing: la evidencia reutilizable es la que un tercero puede inspeccionar y volver a comprobar.

La verificación formal asistida por IA ya merece un piloto cuando existe código crítico, una propiedad acotable y un checker independiente. No merece todavía sustituir el programa de AppSec ni aprobar un sistema completo por asociación. La decisión prudente es construir una escalera: seleccionar un componente, redactar una propiedad útil, fijar el binario, comprobar la prueba fuera del agente y comparar el alcance con producción. Solo después se decide si la garantía entra como evidencia opcional o gate obligatorio.

Si tu equipo necesita convertir agentes de código en una pipeline auditable, el trabajo valioso empieza en el contrato de evidencia: qué puede cambiar el agente, quién revisa el enunciado y qué sistema conserva la decisión. Wasyra diseña flujos de agentes y software a medida con permisos, evaluación y trazabilidad explícitos. El objetivo no es prometer ausencia de bugs; es hacer que cada afirmación técnica tenga un artefacto comprobable detrás.