Technical Summary: Verus-SpecGym

Problem Statement

While AI coding agents are increasingly capable of generating verified code (code accompanied by machine-checked proofs), a fundamental bottleneck remains: the faithfulness of the formal specification itself. Verified code generation guarantees that code satisfies a given formal specification, but it does not guarantee that the specification accurately captures the user's informal intent. If an agent generates a specification that is too weak, it may certify incorrect code; if too strong, it may reject correct code.

The paper addresses specification autoformalization: the task of translating informal programming problems (natural language descriptions) into faithful formal specifications. The core challenge is evaluation. Existing methods rely on expensive expert-written reference specifications or approximate LLM judges, both of which struggle to detect subtle semantic errors or scale effectively. There is a need for a scalable, deterministic evaluation mechanism that can verify whether a generated specification accepts exactly the valid inputs and correct outputs defined by the informal problem.

Methodology

1. The Benchmark: VERUS-SPECBENCH

The authors introduce VERUS-SPECBENCH, a benchmark comprising 581 specification-writing tasks derived from Codeforces programming problems. These problems were selected to target Verus, a verification framework for Rust.

• Task Structure: Each task provides an agent with an informal problem statement, a formal Verus skeleton (defining input/output types and empty pre_spec and post_spec functions), sample test cases, and documentation.
• Data Sources: The benchmark leverages two distinct sources for test cases:
  • Official Codeforces Tests: Used primarily for completeness checks (valid inputs and correct outputs).
  • Codeforces "Hacks": Adversarial inputs written by human competitors to break incorrect solutions that passed official tests. These are critical for soundness checks (identifying invalid inputs or incorrect outputs that models might erroneously accept).

2. The Environment: VERUS-SPECGYM

The evaluation occurs in VERUS-SPECGYM, an agentic environment where models interact with Verus, a bash shell, and a filesystem.

• Iterative Refinement: Agents read the problem, write specifications, and iteratively refine them based on feedback from a custom evaluation command (verus_gym_specgen_check).
• Executable Specifications: A key technical innovation is the extension of Verus's exec_spec mechanism. Verus specifications are typically logical predicates for a theorem prover and cannot be run on concrete inputs. The authors extended exec_spec (specifically introducing exec_spec_unverified!) to compile generated specifications into executable Rust code. This allows the system to run the specification against concrete test cases to determine acceptance or rejection deterministically.

3. Evaluation Framework

The evaluation decomposes faithfulness into four buckets of test cases:

1. Pre-completeness: Valid inputs must be accepted by pre_spec.
2. Pre-soundness: Invalid inputs must be rejected by pre_spec.
3. Post-completeness: Correct (input, output) pairs must be accepted by post_spec.
4. Post-soundness: Incorrect (input, output) pairs must be rejected by post_spec.

The evaluator uses a two-tiered resolution strategy:

• Symbolic Check: Attempts to prove the specification's behavior using Verus's SMT solver.
• Executable Fallback: If symbolic proof is inconclusive, the specification is compiled to executable Rust and run on the concrete test case. This ensures that even complex specifications can be evaluated deterministically.

Key Contributions

1. VERUS-SPECGYM & VERUS-SPECBENCH: The first agentic environment and benchmark specifically designed to evaluate specification autoformalization using executable specifications and adversarial "hack" test cases.
2. Executable Specification Evaluator: A novel extension of Verus's exec_spec mechanism that enables deterministic testing of specification faithfulness without requiring expert-written reference specifications or relying solely on LLM judges.
3. Adversarial Evaluation Suite: The construction of a comprehensive evaluation suite using human-written Codeforces hacks, demonstrating that these adversarial inputs expose specification failures that official tests miss.
4. Empirical Analysis of Failure Modes: A detailed analysis showing that even frontier models capable of generating correct code often fail to write faithful specifications, with failures clustering into omitted input assumptions, accepted incorrect outputs, and rejected valid ones.

Results

The authors evaluated six frontier and open-source language models (including gemini-3.1pro, gpt5.3-codex, opus4.6, and several open-source models) under a fixed compute and time budget.

• Performance Gap: The strongest model, gemini-3.1pro, solved 77.8% of tasks. Other frontier models solved between 51.1% and 57.8%, while open-source models achieved only 21.5%–25.5%.
• Code vs. Specification: On a subset of problems where gpt5.3-codex could generate correct executable code (81.8% success), it failed to write a faithful specification for the same problem in many cases. This indicates that specification autoformalization is a distinct bottleneck separate from code generation.
• Importance of Soundness Tests: Evaluating only on completeness tests significantly overestimates performance. Adding soundness tests (derived from hacks) caused the Pass@1 for gpt5.3-codex to drop from 77.8% to 58% and gemini-3.1pro from 82% to 78%.
• LLM-as-a-Judge Limitations: When using an LLM as a judge to evaluate specifications, it missed 26% of the failures detected by the executable evaluator. This suggests that executable testing is a more reliable signal for the subtle errors inherent in this task.
• Failure Modes: Qualitative analysis revealed three recurring failure patterns:
  1. Omitted Input Assumptions: Missing global structural promises (e.g., assuming a solution exists when it doesn't).
  2. Accepted Incorrect Outputs: Failing to enforce optimality or correctness constraints (e.g., accepting non-coprime pairs).
  3. Rejected Valid Outputs: Writing overly complex or restrictive specifications that reject correct answers.

Significance and Claims

The paper claims that specification autoformalization is within reach for frontier agents but remains brittle, even on problems where they can successfully generate correct code. The work demonstrates that:

• Faithful specification generation is a distinct capability from code generation.
• Executable testing using adversarial inputs (hacks) is essential for reliable evaluation, as it exposes edge cases that standard tests and LLM judges miss.
• Current models struggle with the nuance of translating informal intent into precise logical predicates, often failing to capture implicit constraints or optimality criteria.

The authors position this work as a step toward more robust verified code generation, highlighting that the "bottleneck" has shifted from writing code to writing the right specification. They emphasize that their approach provides a scalable, deterministic signal for faithfulness without the prohibitive cost of expert reference specifications.