Bryan Parno, Pranjal Aggarwal, Seungone Kim, Kanna Shimizu, Anmol Agarwal, Natalie Neamtu, Jannis Limperg, Cedric Flamant, Sean Cmu
We lifted 15 functions out of this paper's own repositories and ran 11 of them in a sandbox. "Ran" means the function executed on a synthesized input and returned a value. It is not a reproduction of the paper's results.
| Repository | Role | Ran |
|---|---|---|
| formal-verif-is-cool/verus-spec-gym | canonical | 11 of 15 |
| Function | Status | Where it lives |
|---|---|---|
| build_task_block | Ran | formal-verif-is-cool/verus-spec-gym/verus_spec_gym_specific_scripts/01_add_task_string.py code served (permissive licence) · get_code("8720a5baa2bda6e9") |
| compare_numeric | Ran | formal-verif-is-cool/verus-spec-gym/adapters/dabstep/scorer.py code served (permissive licence) · get_code("de19ee7afd87e58d") |
| compute_skill_digest | Ran | formal-verif-is-cool/verus-spec-gym/src/harbor/skills.py code served (permissive licence) · get_code("ba5ee1d9b4540911") |
| extract_numeric | Ran | formal-verif-is-cool/verus-spec-gym/adapters/dabstep/scorer.py code served (permissive licence) · get_code("5b8eb1533af10264") |
| is_numeric_with_commas | Ran | formal-verif-is-cool/verus-spec-gym/adapters/dabstep/scorer.py code served (permissive licence) · get_code("a62495edc6f98b22") |
| is_valid_zip | Ran | formal-verif-is-cool/verus-spec-gym/verus_spec_gym_specific_scripts/00_download_tasks_from_drive.py code served (permissive licence) · get_code("6a1371fda6847d50") |
| load_directory_tasks | Ran | formal-verif-is-cool/verus-spec-gym/adapters/reasoning-gym/check_reasoning_gym_registry.py code served (permissive licence) · get_code("59952f68078d5908") |
| load_json_file | Ran | formal-verif-is-cool/verus-spec-gym/verus_spec_gym_specific_scripts/02_calculate_results.py code served (permissive licence) · get_code("7a34caea0b6d9960") |
| load_json_from_zip | Ran | formal-verif-is-cool/verus-spec-gym/verus_spec_gym_specific_scripts/02_calculate_results.py code served (permissive licence) · get_code("5222d192fa6fe184") |
| problem_id_to_task_name | Ran | formal-verif-is-cool/verus-spec-gym/verus_spec_gym_specific_scripts/00_download_tasks_from_drive.py code served (permissive licence) · get_code("35fe44cdfc2044d1") |
| replace_or_insert_task_block | Ran | formal-verif-is-cool/verus-spec-gym/verus_spec_gym_specific_scripts/01_add_task_string.py code served (permissive licence) · get_code("aaaec19d21c1ca6e") |
| compare_tasks | Not yet run | formal-verif-is-cool/verus-spec-gym/adapters/reasoning-gym/check_reasoning_gym_registry.py code served (permissive licence) · get_code("f9cbe74f88c6ad8f") |
| find_zip | Not yet run | formal-verif-is-cool/verus-spec-gym/verus_spec_gym_specific_scripts/00_download_tasks_from_drive.py code served (permissive licence) · get_code("9c8945aa7526c377") |
| load_registry_tasks | Not yet run | formal-verif-is-cool/verus-spec-gym/adapters/reasoning-gym/check_reasoning_gym_registry.py code served (permissive licence) · get_code("ef9a34ebf9f1a20a") |
| resolve_skills | Not yet run | formal-verif-is-cool/verus-spec-gym/src/harbor/skills.py code served (permissive licence) · get_code("9be3a5228f1ec1e0") |
Some links come from the archived Papers with Code dataset (CC BY-SA 4.0): attribution and licence.
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 specification itself matches the user's intent. In this work, we study specification autoformalization: whether language-model agents can translate informal programming problems into faithful formal specifications. We introduce VERUS-SPECBENCH, a benchmark of 581 specificationwriting tasks derived from Codeforces problems and targeting Verus, a verifier for Rust, and VERUS-SPECGYM, an agentic environment in which models interact with Verus, bash, and the filesystem to develop these specifications. The central challenge is evaluation: expert-written reference specifications are expensive to write, and LLM judges can miss subtle mistakes. We address this by (a) extending Verus's exec_spec mechanism so that generated specifications can be executed as Rust code, and (b) testing them against official Codeforces tests and adversarial cases extracted from Codeforces "hacks", which are edge cases written by competitors to break incorrect solutions. On VERUS-SPECBENCH, the strongest frontier model, gemini-3.1pro, solves 77.8% of tasks, other frontier models solve 51.1-57.8%, and open-source models reach only 21.5-25.5%. Our analysis of failure modes shows that model-generated specifications can omit important input assumptions, accept incorrect outputs, and reject valid ones. Separately, we find that LLM-as-a-judge evaluation misses 26% of the failures our evaluator catches. Overall, our results suggest that specification autoformalization is within reach for frontier agents but remains brittle even on problems where they can already generate correct code. The code for running the benchmark, links to the tasks, and the dashboard for trajectory logs can be found at https://github.com/formal-verif-is-cool/verus-spec-gym.
The same record, over MCP at https://syntology.ai/mcp:
get_harvested_code_for_paper("2605.26457")
get_code_for_paper("2605.26457")
have("2605.26457")
Connect an agent — have() is free.