Formal verification of agent-generated code guarantees only that a program satisfies its formal specification, not that the specification faithfully expresses the developer's informal intent. The Verus-SpecGym work (Agarwal et al., 2026) showed that LLM agents can draft Verus specifications for competitive-programming tasks at frontier success rates, but its authors state two unresolved limitations: (i) faithfulness evaluation remains an approximation, because finite test suites cannot rule out all specification errors, so a specification passing every test may still be unfaithful; and (ii) the setting covers only single-file, competition-style problems rather than repository-level, multi-file real-world software. This problem asks for trustworthy specification autoformalization: an operational notion of specification faithfulness together with an evaluation methodology, requiring no expert-written reference specifications, whose acceptance yields a guarantee strictly stronger than finite-test-suite passing, instantiated beyond single-file tasks to repository-level software.

Background

Formal verification uses machine-checked proofs to guarantee that a program satisfies a formal specification: a precondition stating what inputs the code may assume, and a postcondition stating what outputs it must produce. Verus is an open-source verifier for the Rust programming language that checks such specifications automatically by encoding them for an SMT solver (an automated theorem prover for logical formulas over integers, arrays, and other theories). If the proof checks, the code is guaranteed correct — but only relative to the specification; nothing in the pipeline guarantees that the specification itself matches what the developer actually wanted.

Autoformalization is the translation of informal, natural-language statements into formal languages, studied intensively for mathematics in proof assistants such as Lean and Rocq. Specification autoformalization applies this to programs: given an informal problem statement, generate a formal specification. Agarwal et al. (2026) introduced Verus-SpecBench, a benchmark of 581 specification-writing tasks derived from Codeforces competitive-programming problems, and Verus-SpecGym, an agentic environment in which models interact with Verus, a shell, and the filesystem to write specifications. Their central difficulty was evaluation: expert-written reference specifications are expensive, and an LLM-as-judge (an LLM asked to grade the output) missed 26% of the failures their evaluator caught. Their solution was to extend Verus's exec_spec mechanism, which compiles a generated specification into executable Rust code, and to test it against four buckets of concrete cases drawn from official Codeforces tests and from "hacks" — adversarial inputs written by competitors to break incorrect solutions. The buckets check that a specification accepts valid inputs and correct input-output pairs (completeness) and rejects invalid inputs and incorrect outputs (soundness). Their measurements also exposed brittleness: for the model gpt5.3-codex, pass@3 — the fraction of problems solved by at least one of three independent samples — was 75.6%, while pass^3, the fraction solved by all three samples, was only 34.8%.

The authors' stated limitations define the open problem. First, faithfulness evaluation remains an approximation: a finite test suite can expose many specification errors but cannot rule out all of them, so a specification that passes every test may still misstate the intent — meaning a program can be formally verified yet wrong with respect to what was actually wanted. Second, the tasks are single-file, competition-style problems; repository-level specifications for multi-file, real-world software systems are more realistic and may expose additional weaknesses. The surrounding 2026 literature confirms the shape of this gap: VeriContest built a Verus benchmark with expert-validated specifications; SpecSyn, LiveFMBench, Monty, and Coins all evaluate LLM-generated specifications, but each is still test-based, expert-spec-dependent, or heuristic; the only guarantee-style faithfulness certification (Bidirectional Provability Fingerprinting with a PAC-style bound — a probably approximately correct bound that holds with high probability under explicit assumptions) targets mathematical statements in Lean, not program specifications; and repository-level efforts such as BODHI and KaPilot either evaluate against ground-truth specifications or infer specifications from existing code, which risks inheriting the implementation's own flaws rather than formalizing independent intent.

Problem Statement

Establish trustworthy specification autoformalization — the generation and, crucially, the evaluation of formal specifications translated from informal natural-language problem statements — by resolving the two limitations stated by Agarwal et al. (2026):

  1. Faithfulness evaluation beyond finite test suites. Define an operational notion of faithfulness of a formal specification with respect to an informal intent (for example, a semantic equivalence or consistency criterion that accounts for the fact that a natural-language statement admits several admissible formalizations), and construct an evaluation methodology for LLM-generated program specifications that (a) requires no expert-written reference specifications and (b) yields a guarantee strictly stronger than finite-test-suite passing, read operationally: the methodology must reject at least one specification that passes the entire finite test suite yet is unfaithful to the intent, with that rejection itself certified by a proof or by a bound under explicitly stated assumptions. The intent model must be independent of the specification under test, fixed by the informal statement alone and carrying its own stated fidelity criterion.

  2. Extension beyond single-file competition problems. Instantiate the specification-autoformalization task and its evaluation at repository level: multi-file, real-world software systems for which no reference specifications or curated adversarial test suites exist, characterizing how failure modes and evaluation difficulty change relative to the single-file setting.

These two fronts serve one objective — making agent-written formal specifications trustworthy enough that a machine-checked verification against them constitutes evidence about the developer's actual intent rather than only about the specification — and they are mutually dependent: without stronger evaluation (front 1), repository-level results (front 2) cannot even be measured faithfully; without repository-level instantiation, any evaluation guarantee remains untested in the setting where the verified-but-unfaithful risk actually matters. The source work's pass@3 versus pass^3 gap (75.6% versus 34.8% for gpt5.3-codex) is the observed symptom of this trust deficit and motivates the objective above; improved reliability itself is a consequence of, not a substitute for, the evaluation-and-scale objective.

References

  1. Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal, Seungone Kim, Jannis Limperg, Cedric Flamant, Kanna Shimizu, Bryan Parno, Sean Welleck. Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization. arXiv:2605.26457 (DOI 10.48550/arXiv.2605.26457), 2026. https://arxiv.org/abs/2605.26457
  2. Zichen Xie, Mrigank Pawagi, Yuxin Liu, Aaditi Rai, Lize Shao, John Berberian, Sicong Che, Wenxi Wang. VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation. arXiv:2605.08553 (DOI 10.48550/arXiv.2605.08553), 2026. https://arxiv.org/abs/2605.08553
  3. Fanpeng Yang, Xing Li, Shuling Wang, Jie An, Zeyu Sun, Shenghua Feng, Wenhan Wang, Weiyi Wang, Naijun Zhan, Fanjiang Xu. How Powerful are LLMs in Generating Formal Program Specifications? arXiv:2608.13077 (DOI 10.48550/arXiv.2608.13077), 2026. https://arxiv.org/abs/2608.13077
  4. Noor Islam S. Mohammad, Tamim Sheikh. The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements. arXiv:2606.16541 (DOI 10.48550/arXiv.2606.16541), 2026. https://arxiv.org/abs/2606.16541
  5. Hongyi Liu, Madhusudan Parthasarathy, Adithya Murali. Faithful Autoformalization of Natural Language Assertions. arXiv:2607.13303 (DOI 10.48550/arXiv.2607.13303), 2026. https://arxiv.org/abs/2607.13303
  6. Lezhi Ma, Shangqing Liu, Yi Li, Qiong Wu, Han Wang, Lei Bu. SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification. arXiv:2604.21570 (DOI 10.48550/arXiv.2604.21570), 2026. https://arxiv.org/abs/2604.21570
  7. Dong Xu, Jialun Cao, Guozhao Mo, Junjie Hu, Cheng Wen, Hongyu Lin, Xianpei Han, Shengchao Qin, Cong Tian, Shing-Chi Cheung, Le Sun, Yaojie Lu. LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation. arXiv:2605.01394 (DOI 10.48550/arXiv.2605.01394), 2026. https://arxiv.org/abs/2605.01394
  8. Zhiming Chang, Ziyang Li. BODHI: Precise OS Kernel Specification Inference. arXiv:2605.23931 (DOI 10.48550/arXiv.2605.23931), 2026. https://arxiv.org/abs/2605.23931
  9. Minghua Wang, Yuxi Ling, Mingzhi Gao, Yuwei Liu, Lin Huang. KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification. arXiv:2607.21957 (DOI 10.48550/arXiv.2607.21957), 2026. https://arxiv.org/abs/2607.21957