Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization

• URL: http://arxiv.org/abs/2605.26457v1
• Date: Tue, 26 May 2026 02:12:48 GMT
• Title: Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
• Abstract summary: We study specification autoformalization: whether LLM agents can translate informal programming problems into faithful formal specifications.<n>We introduce Verus-SpecBench, a benchmark of 581 spec-writing tasks derived from Codeforces problems.<n>Our analysis of failure modes shows that model-generated specs can accept important input assumptions, accept incorrect outputs, & reject valid ones.
• Score: 26.123396123145415
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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

Related papers

• Schwarz: Solver-Aware Agentic Program Verification [1.9215527229034466]
  Schwarz is an agentic verification harness that makes SMT-backed proof failure local, checkable, and repairable.<n>We implement Schwarz for C and Rust/Verus and evaluate it on 1,475 tasks.
  arXiv  Detail & Related papers  (2026-08-31T13:54:48Z)
• Fantastic Adaptive Taxonomies and How to Use Them [100.20614173157708]
  AdaMAST converts execution traces into a compact, evidence-grounded failure taxonomy.<n>No code is hand-authored, no trace human-annotated.<n>In agent-system search, taxonomy-coded diagnoses of failed candidates outperform free-form.
  arXiv  Detail & Related papers  (2026-07-17T17:41:16Z)
• The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK [0.0]
  In a verifier-driven loop, AI agents wrote and verified bare-metal security software in Ada/SPARK spanning classical and post-quantum cryptography, TLS 1.3, IKEv2, X.509, and a Matrix client.<n>GNATprove discharged 49,280 proof obligations, established functional correctness for selected primitives, and proved the absence of run-time errors for the rest.<n>We report where each layer caught faults and draw the central lesson: what an agent can be trusted to establish is bounded by the strength of its feedback.
  arXiv  Detail & Related papers  (2026-07-15T20:09:05Z)
• Teaching Code LLMs to Reason with Intermediate Formal Specifications [9.552020178028576]
  SpecCoder is a training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces.<n> SpecCoder selects specifications that hold on correct executions while rejecting faulty executions, turning specifications from passive annotations into executable evidence.
  arXiv  Detail & Related papers  (2026-07-05T11:09:30Z)
• ContraFix: Agentic Vulnerability Repair via Differential Runtime Evidence and Skill Reuse [10.503895811137095]
  Large language model (LLM) agents are increasingly used for automated vulnerability repair.<n>Recent empirical results show that these agents still struggle with real-world vulnerabilities.<n>We present ContraFix, an agentic framework that couples runtime evidence with reusable repair skills.
  arXiv  Detail & Related papers  (2026-05-17T13:48:25Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• Project Prometheus: Bridging the Intent Gap in Agentic Program Repair via Reverse-Engineered Executable Specifications [14.657771106188115]
  Current solutions relying on natural language summaries or adversarial sampling often fail to provide the deterministic constraints required for surgical repairs.<n>We introduce textscPrometheus, a novel framework that bridges this gap by prioritizing textitSpecification Inference over code generation.<n>Our framework achieved a total correct patch rate of textbf93.97% (639/680)
  arXiv  Detail & Related papers  (2026-04-19T14:27:27Z)
• CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation [49.30536937161147]
  We introduce CodeSpecBench, a benchmark for executable behavioral specification generation under an execution-based evaluation protocol.<n>CodeSpecBench supports both function-level and repository-level tasks and encodes specifications as executable Python functions.<n>We observe a sharp performance degradation on repository-level tasks, where the best model attains only a 20.2% pass rate.
  arXiv  Detail & Related papers  (2026-04-14T04:31:45Z)
• AutoReSpec: A Framework for Generating Specification using Large Language Models [1.0026496861838448]
  Large Language Models (LLMs) have shown promise in formal specification generation, but early results reveal several limitations.<n>We present AutoReSpec, a collaborative framework that combines open and closed-source LLMs for verifiable specification generation.<n>We evaluate AutoReSpec on a new benchmark of 72 real-world and synthetic Java programs.
  arXiv  Detail & Related papers  (2026-04-04T15:17:08Z)
• Where LLM Agents Fail and How They can Learn From Failures [62.196870049524364]
  Large Language Model (LLM) agents have shown promise in solving complex, multi-step tasks.<n>They amplify vulnerability to cascading failures, where a single root-cause error propagates through subsequent decisions.<n>Current systems lack a framework that can comprehensively understand agent error in a modular and systemic way.<n>We introduce the AgentErrorTaxonomy, a modular classification of failure modes spanning memory, reflection, planning, action, and system-level operations.
  arXiv  Detail & Related papers  (2025-09-29T18:20:27Z)
• Is Your Automated Software Engineer Trustworthy? [0.850206009406913]
  Large Language Models (LLMs) are being increasingly used in software engineering tasks.<n>LLMs respond to every issue and generate a patch for every case, even when the input is vague or their own output is incorrect.<n>This leads to unreliable behaviour, such as hallucinated code changes or responses based on vague issue reports.<n>We introduce BouncerBench, a benchmark that evaluates whether LLM-based software agents can refuse to act when inputs are ill-defined.
  arXiv  Detail & Related papers  (2025-06-21T20:56:20Z)
• CLEVER: A Curated Benchmark for Formally Verified Code Generation [53.5486188696892]
  $rm Csmall LEVER$ is a high-quality, curated benchmark of 161 problems for end-to-end verified code generation in Lean.<n>Each problem consists of (1) the task of generating a specification that matches a held-out ground-truth specification, and (2) the task of generating a Lean implementation that provably satisfies this specification.
  arXiv  Detail & Related papers  (2025-05-20T05:15:47Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  We propose a transformer-based model that answers binary questions over rule-bases and generates the corresponding proofs. Our model learns to predict nodes and edges corresponding to proof graphs in an efficient constrained training paradigm. We conduct experiments on synthetic, hand-authored, and human-paraphrased rule-bases to show promising results for QA and proof generation.
  arXiv  Detail & Related papers  (2020-10-06T15:47:53Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.