Verus-SpecGym: Un entorno agéntico para evaluar la autoformalización de especificaciones

Resumen

Los agentes de codificación basados en IA se utilizan cada vez más para escribir software real, pero garantizar que sus resultados sean correctos sigue siendo un desafío fundamental. La verificación formal ofrece un camino prometedor: un agente genera código junto con una prueba verificada por máquina, garantizando que el código satisface una especificación formal. Sin embargo, no hay garantía de que la propia especificación formal corresponda con la intención del usuario. En este trabajo, estudiamos la autoformalización de especificaciones: si los agentes basados en LLM pueden traducir problemas informales de programación en especificaciones formales fieles. Presentamos Verus-SpecBench, un benchmark de 581 tareas de redacción de especificaciones derivadas de problemas de Codeforces orientados a Verus, un verificador para Rust, y Verus-SpecGym, un entorno agéntico en el que los modelos interactúan con Verus, bash y el sistema de archivos para desarrollar estas especificaciones. El desafío central es la evaluación: las especificaciones de referencia escritas por expertos son costosas de elaborar, y los jueces LLM pueden pasar por alto sutiles errores. Abordamos esto mediante (a) la extensión del mecanismo exec_spec de Verus para que las especificaciones generadas puedan ejecutarse como código Rust, y (b) probándolas contra pruebas oficiales de Codeforces y casos adversarios extraídos de los "hacks" de Codeforces, que son casos límite escritos por competidores para romper soluciones incorrectas. En Verus-SpecBench, el modelo más fuerte, Gemini 3.1 Pro, resuelve el 77.8% de las tareas; otros modelos fronterizos resuelven entre el 51.1% y el 57.8%, y los modelos de código abierto solo alcanzan entre el 21.5% y el 25.5%. Nuestro análisis de modos de fallo muestra que las especificaciones generadas por modelos pueden omitir supuestos importantes de entrada, aceptar salidas incorrectas y rechazar válidas. También encontramos que la evaluación de LLM como juez omite el 26% de los fallos que nuestro evaluador detecta. En general, nuestros resultados sugieren que la autoformalización de especificaciones está al alcance de los agentes fronterizos, pero sigue siendo frágil incluso en problemas donde ya pueden generar código correcto. El código, los datos y los registros se pueden encontrar en https://github.com/formal-verif-is-cool/verus-spec-gym

English

AI coding agents are increasingly used to write real-world software, but ensuring that their outputs are correct remains a fundamental challenge. Formal verification offers a promising path: an agent generates code together with a machine-checked proof, guaranteeing that the code satisfies a formal specification. However, there is no guarantee that the formal spec itself matches the user's intent. In this work, we study specification autoformalization: whether LLM agents can translate informal programming problems into faithful formal specifications. We introduce Verus-SpecBench, a benchmark of 581 spec-writing tasks derived from Codeforces problems targeting Verus, a verifier for Rust, and Verus-SpecGym, an agentic environment in which models interact with Verus, bash, & the filesystem to develop these specs. The central challenge is evaluation: expert-written reference specs are expensive to write, & LLM judges can miss subtle mistakes. We address this by (a) extending Verus's exec_spec mechanism so that generated specs can be executed as Rust code, & (b) testing them against official Codeforces tests & adversarial cases extracted from Codeforces "hacks", which are edge cases written by competitors to break incorrect solutions. On Verus-SpecBench, the strongest model, Gemini 3.1 Pro, solves 77.8% of tasks, other frontier models solve 51.1--57.8% & OSS models reach only 21.5--25.5%. Our analysis of failure modes shows that model-generated specs can omit important input assumptions, accept incorrect outputs, & reject valid ones. We also find that LLM-as-a-judge evaluation misses 26% of the failures our evaluator catches. Overall, our results suggest that spec autoformalization is within reach for frontier agents but remains brittle even on problems where they can already generate correct code. The code, data, & logs can be found at https://github.com/formal-verif-is-cool/verus-spec-gym