Verus-SpecGym : un environnement agentique pour l'évaluation de l'autoformalisation de spécifications

Résumé

Les agents de codage basés sur l'IA sont de plus en plus utilisés pour écrire des logiciels concrets, mais garantir l'exactitude de leurs résultats reste un défi fondamental. La vérification formelle offre une voie prometteuse : un agent génère du code accompagné d'une preuve vérifiée par machine, garantissant que le code satisfait une spécification formelle. Cependant, rien ne garantit que la spécification formelle elle-même corresponde à l'intention de l'utilisateur. Dans ce travail, nous étudions l'autoformalisation des spécifications : la capacité des agents LLM à traduire des problèmes de programmation informels en spécifications formelles fidèles. Nous introduisons Verus-SpecBench, un ensemble de référence comprenant 581 tâches de rédaction de spécifications issues de problèmes Codeforces ciblant Verus, un vérificateur pour Rust, et Verus-SpecGym, un environnement agentique dans lequel les modèles interagissent avec Verus, bash et le système de fichiers pour élaborer ces spécifications. Le défi central réside dans l'évaluation : les spécifications de référence rédigées par des experts sont coûteuses à produire, et les juges LLM peuvent passer à côté d'erreurs subtiles. Nous y remédions en (a) étendant le mécanisme exec_spec de Verus afin que les spécifications générées puissent être exécutées en tant que code Rust, et (b) en les testant face aux tests officiels de Codeforces ainsi qu'à des cas adverses extraits des « hacks » de Codeforces, c'est-à-dire des cas limites écrits par les participants pour briser des solutions incorrectes. Sur Verus-SpecBench, le modèle le plus performant, Gemini 3.1 Pro, résout 77,8 % des tâches ; d’autres modèles de pointe en résolvent 51,1 à 57,8 %, et les modèles open source n’atteignent que 21,5 à 25,5 %. Notre analyse des modes d’échec montre que les spécifications générées par les modèles peuvent omettre des hypothèses d’entrée importantes, accepter des sorties incorrectes et rejeter des sorties valides. Nous constatons également que l’évaluation par LLM comme juge manque 26 % des échecs détectés par notre évaluateur. Dans l’ensemble, nos résultats suggèrent que l’autoformalisation des spécifications est à la portée des agents de pointe, mais reste fragile, même pour des problèmes pour lesquels ils sont déjà capables de générer du code correct. Le code, les données et les journaux sont disponibles à l’adresse 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