Paper deep dive
AutoReSpec: A Framework for Generating Specification using Large Language Models
Ragib Shahariar Ayon, Shibbir Ahmed
Intelligence
Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 97%
Last extracted: 4/10/2026, 2:17:33 AM
Summary
AutoReSpec is a collaborative framework for generating verifiable formal specifications (JML) for Java programs. It uses a dynamic LLM recommender to select model pairs based on program structure and employs a two-stage process: a primary LLM for initial generation and a collaborative LLM for error-guided refinement using validator feedback. The framework outperforms existing tools like SpecGen and FormalBench in success probability and completeness while reducing evaluation time.
Entities (6)
Relation Signals (3)
AutoReSpec → uses → Java Modeling Language
confidence 100% · synthesizing formal specifications in Java Modeling Language (JML)
AutoReSpec → outperforms → SpecGen
confidence 95% · Our results show that it achieves 67 passes out of 72, outperforming SpecGen and FormalBench
AutoReSpec → uses → OpenJML
confidence 95% · Validator: OpenJML & Z3
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Formal specification generation has recently drawn attention in software engineering as a way to improve program correctness without requiring manual annotations. Large Language Models (LLMs) have shown promise in this area, but early results reveal several limitations. Generated specifications often fail verification due to syntax errors, logical inaccuracies, or incomplete reasoning, especially in programs with loops or branching logic. Techniques like SpecGen and FormalBench attempt to address this through prompting and benchmarking, but they typically rely on static prompts and do not offer mechanisms for recovering from failure or adapting to different program structures. In this paper, we present AutoReSpec, a collaborative framework that combines open and closed-source LLMs for verifiable specification generation. AutoReSpec dynamically chooses an LLM pair and prompt configuration based on the structure of the input program. If the primary LLM fails to produce a valid output, a collaborative model is invoked, using validator feedback to refine and correct the specification. This two-stage design enables both speed and robustness. We evaluate AutoReSpec on a new benchmark of 72 real-world and synthetic Java programs. Our results show that it achieves 67 passes out of 72, outperforming SpecGen and FormalBench in both Success Probability and Completeness. Our experimental evaluation achieves a 58.2% success probability and a 69.2% completeness score, while cutting evaluation time by 26.89% on average compared to prior methods. Together, these results demonstrate that AutoReSpec offers a scalable, efficient, and reliable approach to LLM-based formal specification generation.
Tags
Links
- Source: https://arxiv.org/abs/2604.03758v1
- Canonical: https://arxiv.org/abs/2604.03758v1
Trouble viewing inline? Open PDF directly →
Full Text
67,477 characters extracted from source content.
Expand or collapse full text
AutoReSpec: A Framework for Generating Specification using Large Language Models Ragib Shahariar Ayon Texas State University San Marcos, TX, USA ipd21@txstate.edu Shibbir Ahmed Texas State University San Marcos, TX, USA shibbir@txstate.edu Abstract Formal specification generation has recently drawn attention in software engineering as a way to improve program correctness without requiring manual annotations. Large Language Models (LLMs) have shown promise in this area, but early results reveal several limitations. Generated specifications often fail verification due to syntax errors, logical inaccuracies, or incomplete reasoning, especially in programs with loops or branching logic. Techniques like SpecGen and FormalBench attempt to address this through prompting and benchmarking, but they typically rely on static prompts and do not offer mechanisms for recovering from failure or adapting to different program structures. In this paper, we present AutoReSpec, a collaborative framework that combines open and closed-source LLMs for verifiable specification generation. AutoRe- Spec dynamically chooses an LLM pair and prompt configuration based on the structure of the input program. If the primary LLM fails to produce a valid output, a collaborative model is invoked, using validator feedback to refine and correct the specification. This two-stage design enables both speed and robustness. We evaluate AutoReSpec on a new benchmark of 72 real-world and synthetic Java programs. Our results show that it achieves 67 passes out of 72, outperforming SpecGen and FormalBench in both Success Prob- ability and Completeness. Our experimental evaluation achieves a 58.2% success probability and a 69.2% completeness score, while cutting evaluation time by 26.89% on average compared to prior methods. Together, these results demonstrate that AutoReSpec of- fers a scalable, efficient, and reliable approach to LLM-based formal specification generation. CCS Concepts • Software and its engineering→Specification languages; For- mal software verification;• Computing methodologies→Natural language processing; Machine learning. Keywords Specification, Large Language Model, OpenJML ACM Reference Format: Ragib Shahariar Ayon and Shibbir Ahmed. 2026. AutoReSpec: A Frame- work for Generating Specification using Large Language Models. In 2026 This work is licensed under a Creative Commons Attribution 4.0 International License. FORGE ’26, Rio de Janeiro, Brazil © 2026 Copyright held by the owner/author(s). ACM ISBN 979-8-4007-2477-0/2026/04 https://doi.org/10.1145/3793655.3793731 IEEE/ACM Third International Conference on AI Foundation Models and Soft- ware Engineering (FORGE ’26), April 12–13, 2026, Rio de Janeiro, Brazil. ACM, New York, NY, USA, 11 pages. https://doi.org/10.1145/3793655.3793731 1 Introduction Formal specifications play a foundational role in reasoning about program behavior. They enable a range of tasks in software engi- neering, including automated verification [18], test generation [17], and program synthesis [7]. Despite their theoretical value, formal specifications are largely absent in real-world codebases. Writing them by hand requires deep expertise in formal methods, famil- iarity with specification languages like JML [26], and significant time investment, especially for programs with complex control flow or semantic constraints. Several works have explored ways to automate this process [17,19,32,37], with recent work focusing on leveraging LLMs to learn formal specifications directly from code. A number of LLM-based approaches have been proposed for this task. SpecGen [28] applies a few-shot conversational prompting and mutation-based specification generation to improve verification suc- cess. Pei et al. [34] investigate whether LLMs can synthesize induc- tive invariants with fine-tuned models. FormalBench [24] evaluates LLMs on a broader set of semantic reasoning tasks, using specifica- tion synthesis as a proxy for deeper program understanding. While these efforts demonstrate early promise, they face important limita- tions. SpecGen and Pei et al. lack generality across model families and fail to recover when initial specifications are unverifiable. For- malBench, by design, focuses on evaluation rather than generation, and does not investigate interactive or collaborative refinement workflows. None of these systems supports adaptive prompting or dynamic model selection tailored to program complexity. To address these challenges, we introduce AutoReSpec, a col- laborative LLM framework for synthesizing formal specifications in Java Modeling Language (JML). Although AutoReSpec is con- ceptually language-agnostic, supporting any setting where code and specification pairs can be verified, our implementation targets Java and JML due to the availability of mature verification tooling and benchmark datasets. AutoReSpec is built on three key ideas: (1) dynamically selecting the optimal LLM pair (primary and fall- back) and few-shot configuration based on the program type; (2) generating and refining prompts through a conversational loop guided by validator feedback; and (3) selectively invoking a collabo- rative model upon primary-model failure. AutoReSpec first runs the primary LLM in a validator-guided refinement loop; if it still fails within the refinement budget, the last candidate specification and verifier error are forwarded to the collaborative LLM for focused recovery. arXiv:2604.03758v1 [cs.SE] 4 Apr 2026 FORGE ’26, April 12–13, 2026, Rio de Janeiro, BrazilRagib Shahariar Ayon and Shibbir Ahmed State-of-the-art Techniques public class TokenTest02 public static boolean f(String sentence) String[] tokens = sentence.split(" "); int i = 0; for (String token : tokens) if (i == 3) if (!token.equals("genneration")) return false; ++i; return true; Input Java Code public class TokenTest02 //@ ensures ==> (∀ int i; 0 <= i && i < sentence.split(" ").length; i == 3 || !sentence.split(" ")[i].equals("genneration")); //@ ensures ! ==> (∀ int i; 0 <= i && i < sentence.split(" ").length; i != 3 || sentence.split(" ")[i].equals("genneration")); public static boolean f(String sentence) String[] tokens = sentence.split(" "); int i = 0; //@ maintaining 0 <= i && i <= tokens.length; //@ decreases tokens.length - i; for (String token : tokens) if (i == 3) if (!token.equals("genneration")) return false; ++i; return true; Completeness: 0%Success Probability: 0% Avg Time: 106.82 secAvg # Validator Call : 20 SpecGen TokenTest02.java:16: verify: The prover cannot establish an assertion (Postcondition: TokenTest02.java:2:) in method f return true; TokenTest02.java:2: verify: Associated declaration: TokenTest02.java:16: //@ ensures ==> (∀ int i; 0 <= i &&.... 2 verification failures Validator: OpenJML & Z3 public class TokenTest02 /*@ requires sentence != null; @ ensures == (∀ int i; 0 <= i < tokens.length; @ (i == 3 ==> tokens[i].equals(""genneration""))); @*/ public static boolean f(String sentence) String[] tokens = sentence.split("" ""); int i = 0; /*@ loop_invariant 0 <= i && i <= tokens.length; @ loop_invariant (∀ int j; 0 <= j < i; @ (j == 3 ==> tokens[j].equals(""genneration""))); @*/ for (String token : tokens) if (i == 3) /*@ assert token.equals(""genneration""); @*/ if (!token.equals(""genneration"")) return false; ++i; return true; Completeness: 0%Success Probability: 0% Avg Time: 20.09 secAvg # Validator Call : 3 FormalBench ### ERROR TYPES: - Error Type: SyntaxError ``` /tmp/TokenTest02.java:16: error: Expected loop specifications while in JML: assignable is not a loop specification keyword @ assignable \ ; 1 error ``` Validator: OpenJML & Z3 Completeness: 100%Average Time: 33.81 secAverage # Validator Call : 7Success Probability: 80% AutoReSpec TokenTest02.java:9: verify: The prover cannot establish an assertion (LoopInvariant) in method f //@ loop_invariant 0 <= i && i <= tokens.length; 1 verification failure public class TokenTest02 //@ requires sentence != null; public static boolean f(String sentence) //@ requires sentence.length() > 0; String[] tokens = sentence.split(" "); int i = 0; //@ loop_invariant 0 <= i && i <= tokens.length; for (String token : tokens) if (i == 3) if (!token.equals("generation")) return false; i++; return true; Primary LLM Validator: OpenJML & Z3 public class TokenTest02 //@ requires sentence != null; //@ requires sentence.length() > 0; //@ ensures ==> (sentence.split(" ").length > 3 && sentence.split(" ")[3].equals("generation")); //@ ensures ! ==> (sentence.split(" ").length <= 3|| !sentence.split(" ")[3].equals("generation")); public static boolean f(String sentence) String[] tokens = sentence.split(" "); int i = 0; //@ loop_invariant 0 <= i && i <= tokens.length; //@ loop_invariant i <= 3 || (i > 3 && tokens[3].equals("generation")); //@ decreases tokens.length - i; while (i < tokens.length) if (i == 3) if (!tokens[i].equals("generation")) return false; i++; return tokens.length > 3; Collaborative LLM Single-model strategy for all program types Computationally expensive and cost-unaware Limited recovery from verification failures Program-aware dynamic LLM recommendation. Cost-efficient collaborative refinement. Verifier-guided escalation improves robustness. State-of-the-art Techniques AutoReSpec Figure 1: Motivating example illustrating Prior tools like SpecGen and FormalBench fail on the Java methodTokenTest02, achieving 0% success probability and completeness under OpenJML with Z3. In contrast, AutoReSpec ’s collaborative pipeline combining an open-source model with a proprietary fallback yields a correct, verifiable specification with 100% success and completeness, fewer validator calls, and faster runtime. Developing such an end-to-end system poses several technical challenges. First, different programs require different prompt strate- gies and model capabilities. Second, verification failures require error-guided prompt refinement that is both specific enough to re- solve issues and general enough to generalize across models. Third, integrating multiple LLMs and verifier iterations without exces- sive latency or token overflow requires careful prompt truncation, memory management, and recovery logic. AutoReSpec mitigates these challenges through an adaptive recommender for model se- lection, a validator-guided refinement engine for error correction, an efficient prompt management module for context control, and a collaborative fallback mechanism for recovery. Under the dynamic model selection configuration (RQ1), the col- laborative version of AutoReSpec verified 119 out of 120 programs from SpecGenBench, achieving 69.32% success probability (SP) and 60.33 % completeness (C). On the full 72-program benchmark (RQ2) combining SpecGenBench, SV-COMP, and real-world OpenJML issues, AutoReSpec achieved 58.2% SP and 69.2% C, while reduc- ing average generation time by 26.89% compared with prior tools. Validator logs further confirmed stable recovery behavior across diverse program types. Our contributions are as follows: AutoReSpec : A Framework for Generating Specification using Large Language ModelsFORGE ’26, April 12–13, 2026, Rio de Janeiro, Brazil •We propose AutoReSpec, a novel collaborative framework that recommends LLM-model pairs based on program struc- ture and uses verifier-guided conversational refinement to generate verifiable specifications. • We design a collaborative prompt engineering strategy that combines few-shot examples, validator feedback, and auto- mated prompt truncation to support long-context interac- tions and enable targeted error resolution. • We utilize a mutation-based completeness score, success probability, and number of passes, evaluation time to rank the LLMs for recommendation. •We construct AutoReSpecBench, a new benchmark combining real-world GitHub issues, loop-heavy SV-COMP programs, and challenging cases from SpecGenBench, and release a public leaderboard for reproducible evaluation [9]. • We release our full framework [11], including code, dataset, and VS Code extension [13], as an open-source tool chain to support future work in specification generation and LLM- based reasoning. The remainder of this paper is organized as follows. Section 2 presents a motivating example that highlights the key challenges in automated specification generation. Section 3 details the design of the AutoReSpec framework. Section 4 describes the experimental setup, while Section 5 reports the results and analysis. Section 6 reviews related research, and Section 7 discusses threats to validity. Finally, Section 8 concludes the paper. 2 Motivation Automatically generating formal specifications is challenging be- cause formal languages like JML are highly sensitive to syntax and require precise logical consistency. Even small mistakes, such as a misplaced quantifier, an incorrect assignable clause, or a wrong logical operator, can make an otherwise sound specification unver- ifiable. The challenge becomes greater in real-world Java programs that contain complex control flow and subtle loop invariants, which are often difficult to capture correctly in formal terms. Figure 1 illustrates these challenges using theTokenTest02 method, which processes a string of tokens. The goal is to produce valid JML specifications. We compare three setups: SpecGen [28], FormalBench [24], and our proposed AutoReSpec. SpecGen uses few-shot prompting combined with mutation-based validation to iteratively improve JML specifications through verifier feedback. In contrast, FormalBench [24] provides a standardized evaluation framework that benchmarks LLM-generated specifications using fixed prompts and evaluates consistency, completeness, and ro- bustness under semantics-preserving transformations. Following FormalBench, a state-of-the-art (SOTA) benchmark setup, we adopt its specification-generation configuration as one of our baseline configurations, as it frames specification synthesis as a semantic- reasoning task and provides calibrated prompts and verification infrastructure suitable for fair comparison. We evaluated each approach over ten independent trials to cal- culate the success probability (푆푃) and completeness (C), averaging results across runs to account for stochastic model behavior.푆푃 measures the fraction of trials that produce verifiable specifications for a program, whileCrepresents the average ratio of killed to total mutants, indicating fault-detection coverage. Both baseline systems fail in this example: SpecGen generates JML syntax errors, and FormalBench produces semantically inconsistent specifications that fail verification. Both SOTA methods use a single-model strat- egy across all program types, which does not account for program complexity or costs. This example also reflects two broader ob- servations that motivate our design. First, LLM performance is program-type-dependent: models that work well on simple pro- grams can fail on programs with multi-path control flow, which require stronger reasoning about invariants. Second, relying on a single model for all programs is often cost-inefficient, while relying only on smaller models can reduce verification success on harder cases. These observations motivate a dynamic LLM recommender that selects models based on program type and a collaborative strat- egy that uses a cost-efficient primary model with a stronger model invoked only when needed. In contrast, AutoReSpec identifies the program as a multi-path loop and uses its LLM recommender to select Llama 3 as the pri- mary LLM and GPT-4o as the collaborative LLM. It generates an initial candidate and, if verification fails, forwards the last candi- date and validator feedback to the collaborative LLM for recovery. This collaborative step corrects the specification and produces a valid JML-annotated method, achieving 100%푆푃andCwith fewer validator calls and lower runtime. Taken together, the example yields three key takeaways: (1) naive prompting is insufficient for verifiable specification genera- tion, even for simple programs; (2) recovery from validation failure requires guided refinement and verifier feedback; and (3) coordi- nated model collaboration improves accuracy, efficiency, and ro- bustness. These insights directly motivate the design of AutoReSpec, presented in the following section. 3 Framework 3.1 Overview Figure 2 illustrates the overall architecture of AutoReSpec, which automates the generation of verifiable JML specifications through a structured, validator-guided workflow. The framework consists of four main components: (1) LLM recommender, (2) primary LLM, (3) iterative refinement, and (4) collaborative LLM, followed by an (5) output stage that produces the final verified specification and execution log. This design enables AutoReSpec to adaptively select appropriate models, refine specifications using validator feedback, and coordinate multiple LLMs to generate correct and verifiable results. The overall procedural flow is summarized in Algorithm 1, which formalizes the iterative refinement process used by both LLMs. The notation for the Algorithm is mentioned in Table [8]. Given an input Java programJ, theLLM recommenderfirst analyzes its abstract syntax tree (AST) or equivalent structural representation to infer the program’s type and selects a suitable pair of language models for specification generation. The primary LLM is responsible for the initial synthesis of formal specifications, while the collaborative LLM acts as a fallback when verification fails. The Prompt generatorconstructs and manages all prompts used by these models, including initial prompts with few-shot examples and subsequent refinement prompts that incorporate validator feedback. FORGE ’26, April 12–13, 2026, Rio de Janeiro, BrazilRagib Shahariar Ayon and Shibbir Ahmed Collaborative LLM Initial Prompt Generator Validator Error Annotated Java Code System Message Few-Shot Examples Few-Shot Examples Few-Shot Examples Failed (G.I. > M.I) Next Prompt Few-Shot Examples Few-Shot Examples Previous Prompts Annotated Java Code Generate Guidance Prompt Validator Error Check Error Primary LLM Initial Prompt Generator System Message Few-Shot Examples Few-Shot Examples Few-Shot Examples Input Java Code Annotated Java Code openJML Extract Validator output Annotated Java Code openJML Extract Validator output Passed Primary LLM Collaborative LLM 2 Primary LLM 3 Iterative Refinement 4 Collaborative LLM Input Java Code Ranked List Extract Program Type 1LLM Recommender AST Get LLM Pair Annotated Java Code 5 Output Annotated Java Code Error Logs Failed (G.I. <= M.I.) Figure 2: Overview of AutoReSpec framework Each LLM iteratively generates, validates, and refines specifications until a verifiable output is produced or the iteration limit is reached. When the primary LLM cannot generate a valid specification, AutoReSpec triggers the collaborative phase. The collaborative LLM receives only the final invalid specification and its associated valida- tion feedback from the primary phase, allowing focused correction without redundant context. Both phases follow the same refine- ment protocol, ensuring consistency while improving efficiency and verification success. By combining adaptive model selection with validator-guided refinement, AutoReSpec achieves an efficient two-phase generation process that progressively converges to verified specifications. 3.2 Dynamic LLM Selection via Recommendation TheLLM recommenderserves as an adaptive selection mechanism that identifies the most suitable pair of LLMs for a given program. To determine the appropriate LLMs, the framework first constructs an abstract syntax tree (AST) of the input program to capture its structural hierarchy. Using a rule-based parser, the program type extractor classifies the code into one of five categories [28,41]: Sequential, Branched, Single-path Loop, Multi-path Loop, or Nested Loop. These categories reflect different control-flow complexities that influence the difficulty of generating the specification. To empirically establish model preferences for each program type, we conducted a lightweight calibration study prior to full- scale evaluation. For every program category, three representative samples were randomly selected and evaluated across all candi- date LLMs using identical prompting and validation configurations. For each model, we computed effectiveness metrics: Success Rate Percentage (푆푅), completeness (C), and efficiency metrics: number of validator calls (푁 val ) and mean generation time. These statistics were then aggregated to form a ranked list of model performance per program type. Based on this ranking, theLLM recommenderadopts a cost-aware pairing strategy by default: it assigns a smaller, faster model as the primary LLM for initial specification synthesis, and a higher- capacity or costlier model as the collaborative LLM for recov- ery when verification fails. This configuration balances efficiency and reliability while minimizing redundant computation. TheLLM recommenderalso determines an appropriate few-shot configu- ration specifying the number and selection strategy of examples tailored to the LLM. While AutoReSpec uses cost-effectiveness as its default selection policy, users can customize the ranking criteria to prioritize alternative objectives such as accuracy, latency, or energy efficiency, depending on their application requirements. This recommendation mechanism ensures that each test case is handled by an optimized pair of LLMs, balancing efficiency, model diversity, and success probability rate. 3.3 Prompt Construction and Refinement After the LLM pair and few-shot configuration are determined by theLLM recommender, thePrompt generatorconstructs and re- fines the input prompts for both models. ThePrompt generator generates the input prompts used by both the primary and collabo- rative LLMs. For the initial prompt to the primary LLM, AutoReSpec combines the primary LLM’s system message, a configurable num- ber of few-shot examples (as determined by theLLM recommender described in section 3.2), and a specification generation prompt that includes the input Java code. The few-shot examples are randomly chosen from a curated set of expert-validated specifications. These examples provide structural and formatting cues, enabling the LLM to produce well-structured responses with correctly delimited code blocks that can be programmatically extracted [14]. The system prompt, format of the few-shot examples, and the final specification generation prompts are shown in [10]. The collaborative LLM is invoked only when the primary LLM fails to produce a valid specification. Its objective is to correct the validation error identified by the validator and generate a revised, valid specification. The initial prompts for the collaborative LLM closely resemble those of the primary LLM, with additional in- structions. The system prompt for the collaborative LLM includes instructions to synthesize the validation error and produce a cor- rected specification within a single code block. The initial prompts also include a configurable number of few-shot examples similar to those of the primary LLM. Additionally, it incorporates an initial error feedback prompt instead of a specification generation prompt, as illustrated in [10]. The final failed output from the primary LLM, AutoReSpec : A Framework for Generating Specification using Large Language ModelsFORGE ’26, April 12–13, 2026, Rio de Janeiro, Brazil Algorithm 1: Simplified high-level AutoReSpec workflow Input: Java codeJ , model recommenderR, prompt generatorP, few-shot examplesF, system prompts P ps andP cs , validatorV, error analyzerE 퐴 , iteration limits 퐼 Pmax and 퐼 Cmax . Output: Annotated Java codeJ A , final validation errorsE, iteration statistics, and logsL. 1 Function RefinePhase(J,M,P,P 푠 ,F , 퐼 max ): 2 푝푟표푚푝푡 (0) ←P.initial(P 푠 ,F,J); 3 L ← initLog(푝푟표푚푝푡 (0) ); 4 푝푟표푚푝푡 ← 푝푟표푚푝푡 (0) ; 5 for 푖 ← 1 to 퐼 max do 6 J A ←M(푝푟표푚푝푡) ; 7 E ←V(J A ); 8 L.append(J A ,E); 9if E=∅ then 10returnJ A ,∅,푖,L; 11end 12푝푟표푚푝푡 푔 ←P.guidance(E 퐴 (E)); 13푝푟표푚푝푡 ←P.refine(푝푟표푚푝푡,J A ,E,푝푟표푚푝푡 푔 ); 14 L.append(푝푟표푚푝푡); 15 end 16 returnJ A ,E,퐼 max ,L; 17 푇 ←R.getProgramType(J); 18 (M 푃 ,M 퐶 ) ←R.getModels(푇); 19 (J A ,E,퐼 Pused ,L 푃 ) ← RefinePhase(J,M 푃 ,P,P ps ,F,퐼 Pmax ); 20 if E≠∅ then 21 (J A ,E,퐼 Cused ,L 퐶 ) ← RefinePhase(J A ,M 퐶 ,P,P cs ,F,퐼 Cmax ); 22 L ←L 푃 ∪L 퐶 ; 23 end 24 else 25 L ←L 푃 ; 26 end 27 returnJ A ,E,퐼 Pused ,퐼 Cused ,L; along with the associated validator error, provides the collaborative LLM with complete context to attempt recovery. For iterative refinement as described in 3.4, thePrompt generator extracts the validation error message generated by the validator (OpenJML) and identifies the corresponding error types. Based on these error types, it generates an error-specific guidance message with refinement examples or falls back to a generic guidance mes- sage. This guidance message is then combined with the previously generated invalid JML-annotated code and the validation error to form the next iterative prompt. Additionally, the constructor retains previous prompt messages to maintain conversational continuity across iterations. LLMs tend to hallucinate more, incur higher computational costs, and exhibit slower response times as the number of input tokens increases. This results from the quadratic attention complexity in transformer architectures, making long-context inference significantly more expensive [21,27]. To reduce the context window for proprietary models, thePrompt generatoralso employs automated prompt truncation to remain within the model constraints. AutoReSpec retains only the last few prompts or truncates prompts to 4000 tokens, whichever comes first, ensuring both compactness and contextual relevance during iterative refinement. 3.4 Collaborative LLMs for Iterative Specification Generation After the prompt templates are defined by thePrompt generator, AutoReSpec executes the specification generation process in two sequential phases, led by a primary and a collaborative LLM. Hal- lucinations remain a significant challenge in LLMs, but they can be mitigated through conversational prompting, which helps align model outputs with user intent and maintain contextual consis- tency [43]. Following the prompting strategy of Xia et al. [40], AutoReSpec interacts with LLMs in a conversational manner to gen- erate formal specifications. By iteratively incorporating validation errors and relevant guidance messages into the prompts, the models refine their outputs over successive turns. This approach not only helps reduce syntax errors but also provides a mechanism for ad- dressing semantic verification errors, often improving specification accuracy and completeness. The specification generation process begins with the primary LLM recommended by theLLM recommenderfor the queried pro- gram type. The initial prompt for this LLM is generated byPrompt generator and sent to the selected model to produce a specification. Each generated specification is immediately verified; if validation fails, thePrompt generatorparses the error messages, retrieves relevant guidance, and reconstructs the next prompt for iterative refinement. This conversational loop continues until a valid specifi- cation is produced or the primary iteration limit is reached. If the primary LLM fails to generate a correct specification within its allotted iterations, AutoReSpec performs a controlled memory reset before invoking the collaborative LLM. This resets the full con- versational history from the primary phase while retaining only the latest invalid specification and its corresponding validation errors. ThePrompt generatorthen constructs an initial collaborative prompt combining this minimal context with few-shot examples and the associated verification feedback. The collaborative LLM, also selected by theLLM recommender, begins reasoning afresh to refine the failed specification. Since it receives only task-relevant input rather than the full conversation history, the collaborative model avoids bias or context drift while maintaining efficiency. If the collaborative LLM succeeds, the verified specification is re- turned; otherwise, the final invalid output and verification errors are provided as a starting point for manual refinement. 4 Experimental Design We evaluate AutoReSpec by formulating the following research questions (RQs) and outlining our approach to answering them: •RQ1: How applicable is collaborative-LLM strategy for generating specifications? •RQ2: How effective is AutoReSpec in generating formal specifications compared to state-of-the-art LLM-based specification generation tools? FORGE ’26, April 12–13, 2026, Rio de Janeiro, BrazilRagib Shahariar Ayon and Shibbir Ahmed •RQ3: How efficient is AutoReSpec in generating speci- fications compared to existing automated tools? • RQ4: How effectively does AutoReSpec resolve verifica- tion failures compared to state-of-the-art approaches? 4.1 Implementation We used Ollama to run open-source LLMs locally and accessed proprietary models (Claude 3.7 Sonnet, GPT-4o) via Anthropic and OpenAI APIs. Based on prior findings [14], we set the temperature to 0.4 for all models. AutoReSpec currently targets Java, prompting LLMs to produce JML annotations that OpenJML 21.0.8 verifies us- ing z3 4.3.1 as its SMT solver [1]. Because OpenJML can hang or fail, we imposed a 180-second timeout per verification. For complete- ness measurement, we used Major 3.0.1 [22] and applied EMS [23] to filter out equivalent mutants, ensuring only semantically dis- tinct faults are counted [25]. All experiments were run on a 28-core Intel® Xeon® W-3465X CPU (2.50 GHz), 256 GB of RAM, and an NVIDIA RTX 6000 Ada Generation GPU under Ubuntu 24.04.2 LTS. Except where noted (Major requiring OpenJDK 11), we used OpenJDK 21.0. 4.2 Dataset Following prior work [6], to thoroughly evaluate AutoReSpec, we develop a new benchmark dataset, AutoReSpecBench, consisting of challenging Java classes drawn from SpecGenBench, SV-COMP [28, 35], and real-world cases from GitHub issues. Importantly, many benchmark instances are multi-method classes rather than only single-function programs, which helps assess whether AutoReSpec scales beyond single-procedure settings. From SpecGenBench, we select 26 programs that LLMs struggle with most in our preliminary experiments. We additionally extract 29 SV-COMP programs fea- turing loop-intensive control flow. To further evaluate real-world applicability and reduce the likelihood of training-set overlap, we include 17 new multi-method Java classes curated from OpenJML GitHub issues [2], reflecting complex verification scenarios encoun- tered in practice. Overall, AutoReSpecBench spans diverse control- flow patterns and common data types (e.g., arrays and strings), and includes varied specification constructs (e.g., postconditions and loop invariants) with both linear and nonlinear relationships among variables. 4.3 Evaluation Metrics Following previous works [25,28], we utilize the metrics of Number of Passes, Success Rate, Success Probability, Number of Verifier Calls, and Completeness to assess AutoReSpec. Number of Passes (푁푃): The number of passes (푁푃) counts the number of programs in the dataset for which at least one gener- ated specification is successfully verified within the allotted budget across trials [28] (i.e., the verifier reports no errors). We define the Success Rate (푆푅) as the dataset-normalized form of this metric: 푆푅= 푁푃 |D| , where|D| is the dataset size. Success Probability (푆푃): The Success Probability metric cap- tures how often an LLM-based approach produces a verifiable spec- ification when run multiple times on the same program. Because LLM outputs can vary from run to run [33], we execute each pro- gram ten times and record the fraction of runs that pass verification. This average success probability summarizes a model’s reliability across the dataset. Number of Verifier Calls (푁 val ): The Number of Verifier Calls metric tracks the number of times the verifier is invoked during specification generation. It serves as a proxy for computational effort: fewer calls indicate that a technique needs fewer refinement attempts to produce a correct specification. For AutoReSpec, we av- erage the sum of primary and collaborative verifier invocations over multiple trials and programs, yielding a single value that reflects overall verifier usage and efficiency. Completeness (C): The Completeness metric [24] evaluates how well a specification detects injected faults via mutation testing. For each verified specification, we generate a set of non-equivalent mutants and count how many trigger verifier errors. A higher completeness score indicates broader fault coverage. Averaging over multiple trials and programs yields an overall completeness percentage. 5 Results and Evaluation 5.1 RQ1: Applicability of the Collaborative LLM Strategy Experimental Setup: We evaluate both individual and collaborative LLM configurations for formal specification generation on SpecGen- Bench [28]. We report the number of passes (푁푃), which indicates how many tasks successfully passed validation from the dataset, as well as Success Probability (푆푃), and completeness (C), both measured over validated programs only. All individual models are tested with zero-, two-, and four-shot prompting, while the top open-source models (Llama 3 (8B), Phi 4 (14B), and Gemma 3 (27B)) are also assessed with conversational prompting. Overall, we tested 120 issues with ten trials each to compute푆푃, andC. To ensure a fair comparison between conversational and collaborative settings, we set the maximum number of validator calls to 10. For collaborative prompting, the budget is evenly divided between the primary and collaborative LLMs. In the Dynamic LLM†configuration, we use ten iterations for both the primary and collaborative LLMs. For dynamic LLM selection, we select the highest-scoring model configuration for each program type. For Sequential and Branched programs, we select Gemma 3, with GPT-4o (Sequential) and Claude-3.7-Sonnet (Branched) as counterparts; for Single- and Multi-path loops, we select Llama 3 and GPT-4o; and for Nested loops, we select Llama 3 and Claude-3.7-Sonnet. To keep our study’s costs under budget, fol- lowing prior work [31], we do not evaluate closed-source LLMs in the individual conversational setting and instead use the individual evaluation setting as a basis for dynamically selecting the LLM. Result Analysis: From Table 1, collaborative prompting achieves higher overall verification coverage and produces more consistent specifications compared to other configurations. AutoReSpec with collaborative prompting and dynamic model selection reaches an 푁푃of 119 out of 120 programs, surpassing the state of the art, SpecGen [28], with 100. A controlled ablation on Llama 3 (8B) evaluates zero, two, four- shot, conversational, and collaborative prompting. Zero-shot per- formance is poor (푁푃= 67,푆푃= 49.55%,C= 10.74%) because the model fails to infer structure without exemplars. Two and four-shot prompting improves both푆푃andC(up to 57 passes and 42.30%). AutoReSpec : A Framework for Generating Specification using Large Language ModelsFORGE ’26, April 12–13, 2026, Rio de Janeiro, Brazil Table 1: Performance of LLM-generated specifications on the SpecGenBench dataset under different prompting settings in AutoReSpec ModelPrompting 푁푃 푆푃 (%) C (%) Individual Claude-3.7-Sonnet Zero-shot6269.8489.84 Two-shot7474.4691.02 Four-shot7674.7489.86 GPT-4o Zero-shot7475.2785.62 Two-shot7678.8281.79 Four-shot7976.5884.05 Llama 3 (8B) Zero-shot6749.5510.74 Two-shot5337.3647.72 Four-shot5740.8842.30 Conv.10364.6629.92 Gemma 3 (27B) Zero-shot4163.9036.51 Two-shot6258.8779.54 Four-shot6159.6782.01 Conv.7769.6177.94 Phi 4 (14B) Zero-shot4542.2234.81 Two-shot5854.1475.80 Four-shot5754.9172.97 Conv.8554.8263.17 Llama 3.3 (70B) Zero-shot4337.9158.49 Two-shot6044.5087.44 Four-shot5455.9389.58 Mistral (7B) Zero-shot1210.006.38 Two-shot4029.2556.31 Four-shot4426.5960.21 Collab. Llama 3 & Llama 3Four-shot10523.1021.38 GPT-4o & GPT-4oFour-shot9462.42 84.84 Dynamic LLM† Few-shot 119 69.3260.33 Note:† Primary & collaborative iterations = 10; Collab. = Collaborative Prompting; Conv. = Conversational; 푁푃 = Passes; 푆푃 = Success Probability; C = Completeness. Individual conversational prompting further increases the number of passes (푁푃= 103,푆푃= 64.66%), while collaborative prompting achieves the highest푁푃(105) with moderate completeness (C= 21.38%). This confirms that collaboration, even between identical models, improves the number of passes without additional itera- tions. The dynamic LLM†configuration extends this by adaptively selecting between two and four-shot prompts, achieving the best 푁푃(119) and a competitive푆푃(69.32%), indicating improved con- sistency and robustness across diverse program types. For proprietary models, GPT-4o and Claude 3.7 Sonnet per- form strongly under individual prompting. GPT-4o attains푁푃= 79,푆푃= 76.58%, andC= 84.05%, while Claude 3.7 achieves푁푃 = 74,푆푃= 74.46%, and the highestC= 91.02%. In the collabora- tive–conversational setup, GPT-4o improves to푁푃= 94 andC= 84.84%. Across open-source models, we observe consistent gains from zero to few-shot and conversational prompting. Llama 3 (8B), Gemma 3 (27B), and Phi 4 (14B) benefit from structured prompting and validator-guided refinement. Llama 3.3 (70B) achieves high com- pleteness under four-shot prompting but lower푆푃(55.93%) and 푁푃, suggesting that model size alone does not guarantee stronger generalization. Mistral (7B) performs weakest across all metrics, highlighting the importance of scale and prompt design. Overall, collaborative prompting with dynamic model selection achieves the best balance across푁푃,푆푃, andC, showing that struc- tured collaboration and adaptivity improve verification outcomes without increasing iteration count. Answer to RQ1: The collaborative-LLM strategy is effective for specification generation. AutoReSpec achieves 119 verified passes compared to SpecGen’s 100, with a 69.32% success prob- ability and 60.33% completeness. These results indicate that structured collaboration and adaptive model selection improve verification outcomes and practicality without increasing the iteration budget. 5.2 RQ2: Effectiveness of AutoReSpec Experimental Setup: To assess the effectiveness of AutoReSpec, we evaluate it against two state-of-the-art LLM-based specification generation techniques, SpecGen and FormalBench. Experiments are conducted on AutoReSpecBench using푆푅%,푆푃, andC, where푆푃 andCare computed only for programs with valid JML annotations. For statistical validation, we use McNemar’s test for paired pass/- fail outcomes [30], and the paired Wilcoxon signed-rank test for per-program푆푃andC[38]. To ensure a fair runtime comparison, we cap SpecGen’s validator calls at 20 and reduce the inter-call delay from 20s to 1s; AutoReSpec uses the dynamic model selection configuration. Branched SequentialSingle-path Loop Nested LoopMulti-path Loop 0 20 40 60 80 100 Success Rate (%) 0.0 33.3 31.6 11.8 11.5 100.0 83.3 89.5 76.5 73.1 100.0 83.3 94.7 88.2 96.2 FormalBenchSpecGenAutoReSpec Figure 3: Pass percentage (푆푅%) across program types for state-of-the-art specification generation techniques. Result Analysis: Figure 3 presents the푆푅% of all techniques on AutoReSpecBench, showing that AutoReSpec matches or exceeds FORGE ’26, April 12–13, 2026, Rio de Janeiro, BrazilRagib Shahariar Ayon and Shibbir Ahmed Success ProbabilityCompleteness 0 20 40 60 80 100 Percentage (%) 24.3% 52.0% 51.4% 63.8% 58.2% 69.2% FormalBenchSpecGenAutoReSpec Figure 4: Average Success Probability and Completeness across LLM-based specification generation techniques. both SpecGen and FormalBench across all program categories. Au- toReSpec achieves notable gains in program types that are generally challenging for LLMs, particularly those involving loops. For Multi- path Loops, AutoReSpec produced 25 valid specifications out of 26, compared to SpecGen’s 19 and FormalBench’s 3 (a 23.1% improve- ment over the best baseline). For Nested Loops, it achieved 15 passes out of 17, exceeding SpecGen (13) and FormalBench (2) by 11.8%. In Single-path Loops, AutoReSpec verified 18 of 19 programs, surpass- ing SpecGen (17) and FormalBench (6) with a 5.3% gain. On less complex categories, AutoReSpec matched SpecGen’s performance, successfully passing all 4 Branched programs and 5 of 6 Sequential programs. These results indicate that AutoReSpec performs robustly across diverse program structures, with consistent improvements on programs featuring complex control flow. Figure 4 reports the average success probability (푆푃) and com- pleteness (C) across techniques. Leveraging dynamic model selec- tion and collaborative prompting, AutoReSpec attains the highest average푆푃(58.2%), exceeding SpecGen (51.4%) and FormalBench (24.3%). AutoReSpec also achieves the highest average completeness, which is approximately 5.4% higher than SpecGen and substantially higher than FormalBench. Overall, AutoReSpec yields more reliable and comprehensive specifications in aggregate, with statistically significant gains over FormalBench. Since all techniques are evaluated on the same programs, we apply paired statistical tests. For pass/fail coverage (SR/NP), Mc- Nemar’s test shows AutoReSpec improves over SpecGen (푝=0.049; 13 vs. 4 discordant passes;Δ푆푅=0.125, 95% CI [0.014, 0.236]) and strongly outperforms FormalBench (푝<10 −15 ; 54 vs. 0;Δ푆푅=0.75, 95% CI [0.653, 0.847]). For푆푃andC, paired Wilcoxon tests show sig- nificant gains over FormalBench (푝<10 −11 ), but not over SpecGen (푝=0.067 for 푆푃 , 푝=0.260 forC). Answer to RQ2: AutoReSpec generates valid specifications for 67 of 72 programs, compared to SpecGen’s 58 and FormalBench’s 13. It achieves the highest overall average success probability and completeness, with statistically significant gains over For- malBench and significantly higher pass coverage than SpecGen. 5.3 RQ3: Efficiency of AutoReSpec Experimental Setup: We evaluate the efficiency of AutoReSpec against SpecGen and FormalBench using the same benchmark programs and experimental setup described in Section 5.2 to ensure consis- tency. We report the average evaluation time (푇 eval ) and number of validator calls (푁 val ). To maintain fairness, SpecGen’s delay be- tween successive LLM calls is reduced from 20 seconds to 1 second, and its validator calls are capped at 20. For AutoReSpec, we employ the dynamic model selection configuration. In this evaluation, since all open-source LLMs were executed on our local hardware with- out per-request API charges, we do not report monetary cost for open-source models. 050100150200250 Average Evaluation Time (s) 0 20 40 60 80 100 Success Rate (%) AutoReSpec - Branched AutoReSpec - Multi-path Loop AutoReSpec - Nested Loop AutoReSpec - Sequential AutoReSpec - Single-path Loop SpecGen - Branched SpecGen - Multi-path Loop SpecGen - Nested Loop SpecGen - Sequential SpecGen - Single-path Loop FormalBench - Branched FormalBench - Multi-path Loop FormalBench - Nested Loop FormalBench - Sequential FormalBench - Single-path Loop Figure 5: Average evaluation time and success rate percentage across different program types of LLM-based specification generation techniques. Result Analysis: As shown in Figure 5, AutoReSpec achieves a balanced trade-off between runtime efficiency and verification suc- cess among the three techniques. Although FormalBench has the shortest average runtime (19.8 s), its low success probability (18.1%) limits practical use. Its validator calls are capped at 3, and it uses 2.38 on average in our experiments. SpecGen requires 111.3 s on average and achieves 80.1% success probability, while AutoReSpec completes evaluation in 109.7 s with a higher success probability of 94.5%. Despite using slightly more validator calls (12.4 vs. 8.2), the adaptive selection mechanism in AutoReSpec reduces redundant refinements, resulting in a marginally faster overall runtime. Al- though FormalBench has the shortest average runtime (19.8 s), its low success probability (18.1%) limits practical use. FormalBench also operates under a small validator-call budget (capped at 3), and in our experiments, it used 2.38 validator calls on average. In terms of API costs for proprietary models, AutoReSpec av- erages $0.13 per Java class, which is lower than SpecGen ($0.16) and FormalBench ($0.17). Costs scale moderately with program complexity, ranging from $0.11 for sequential programs to $0.25 for multi-path loops, and are capped at $0.31 for the most complex cases. Because AutoReSpec prioritizes open-source models and invokes proprietary ones only when necessary, it maintains verification quality while controlling overall cost. These results suggest that efficiency gains primarily arise from the dynamic LLM selection mechanism, which reduces redundant validation loops by choosing suitable prompt configurations for each task. Runtime grows approximately linearly with validator AutoReSpec : A Framework for Generating Specification using Large Language ModelsFORGE ’26, April 12–13, 2026, Rio de Janeiro, Brazil calls and remains bounded by the iteration cap, indicating good scalability to larger codebases. Answer to RQ3: AutoReSpec achieves runtime efficiency com- parable to SpecGen (109.7 s vs. 111.3 s) while using slightly more validator calls on average (12.4 vs. 8.2). Despite this, it remains marginally faster overall and incurs a lower average API cost ($0.13 per Java class), indicating practical efficiency, cost-effectiveness, and scalability. 5.4 RQ4: Error Resolution Capabilities of AutoReSpec Experimental Setup: To better understand the challenges each tech- nique faces during specification generation, we conducted a verifica- tion error type–level struggle analysis. Each verification error type (e.g., Postcondition, LoopInvariantBeforeLoop) represents a distinct class of JML validation failure. We compute the struggle ratio as the frequency of each error type relative to the total number of validator calls across all specifications, quantifying how persistently difficult each category is for a given technique. For AutoReSpec, we used the dynamic model selection configuration. We also manually examined cases where AutoReSpec failed to produce verifiable specifications to identify recurring error patterns and root causes. 051015202530 Struggle Ratio (%) Precondition LoopInvariant PossiblyNegativeIndex NullField LoopInvariantBeforeLoop PossiblyTooLargeIndex Postcondition 1.89 4.41 3.08 8.48 1.16 11.81 6.55 1.44 1.56 7.56 3.50 16.67 13.89 27.06 AutoReSpecSpecGen Figure 6: Top verification error types and struggle ratios (%) for AutoReSpec and SpecGen. Result Analysis: Figure 6 compares struggle ratios for seven common verification error types across SpecGen and AutoReSpec. Postcondition errors remain the most persistent overall: SpecGen records a 27.06% struggle ratio, while AutoReSpec reduces this to 6.55%, indicating stronger handling of functional correctness con- straints. Similarly, for LoopInvariantBeforeLoop, AutoReSpec achieves 1.16% compared to SpecGen’s 16.67%, suggesting more consistent reasoning over iterative control structures. For index-related cate- gories (PossiblyTooLargeIndex and PossiblyNegativeIndex), AutoRe- Spec achieves lower ratios (11.81% vs. 13.89% and 3.08% vs. 7.56%), reflecting improved handling of array bounds. However, AutoRe- Spec shows a higher ratio for NullField errors (8.48% vs. 3.50%), indicating an area where null-safety inference could be enhanced. For other types, such as LoopInvariant and Precondition, both tech- niques exhibit similarly low ratios. A closer inspection of the few failed cases revealed recurring issues mainly related to JML syntax and complex control dependen- cies. The most frequent failure patterns include Precondition, Assert, LoopInvariantBeforeLoop, Postcondition, and InvariantLeaveCaller. In one representative case (TransposeMatrix), a catastrophic JML internal failure occurred due to double rewriting of identifier refer- ences. These failures often occur in programs with deeply nested loops and interdependent postconditions, where current LLMs still struggle to maintain consistency between inferred invariants and postconditions. Overall, the results suggest that AutoReSpec mitigates several per- sistent verification challenges, especially those involving postcon- ditions and loop invariants, while leaving room for improvement in null-safety reasoning. Answer to RQ4: AutoReSpec achieves lower struggle ratios across most verification error types compared to SpecGen, par- ticularly for Postcondition (27.06% vs. 6.55%) and LoopInvari- antBeforeLoop (16.67% vs. 1.16%). These results indicate im- proved error resolution capacity through LLM-guided refine- ments while maintaining robustness across complex program structures. Limitation Because AutoReSpec relies on LLMs’ code under- standing, it inherits their weaknesses. LLMs can misinterpret com- plex control flow [25], sometimes return altered or incomplete code (necessitating expert review), and may omit code entirely, which adds post-processing overhead. On the verification side, OpenJML can produce catastrophic errors on programs with matrix oper- ations, and its SMT solver (Z3) may time out on complex proof obligations, yielding inconclusive results. Finally, our complete- ness measurement uses Major with Equivalent Mutant Suppres- sion (EMS) [23], but EMS does not catch every equivalent mutant, slightly lowering completeness scores and increasing evaluation time. 6 Related Work Recent advances in LLMs have revived interest in automated speci- fication generation and verification. This section scopes our work within three areas of related research: (1) LLM-assisted specification inference, (2) traditional static and dynamic approaches to specifi- cation mining, and (3) evaluation frameworks and benchmarks for verifying specification quality. 6.1 Specification Generation with LLMs LLMs have shown promise in software engineering tasks such as code generation [42], summarization [4], and defect predic- tion [20], motivating their application to formal specification in- ference [15,34]. SpecGen [28] employs conversational prompting with few-shot examples and a mutation-based process that applies heuristic selection to obtain verifiable JML specifications. Other recent studies [15,34,37] explore integrating LLMs with static anal- ysis or ranking mechanisms to improve invariant quality, but they remain limited to single-model or fixed-prompt configurations. Au- toReSpec advances this direction through collaborative prompting for cross-model refinement and adaptive model selection based on program type and validator feedback, demonstrating that prompt FORGE ’26, April 12–13, 2026, Rio de Janeiro, BrazilRagib Shahariar Ayon and Shibbir Ahmed design, fallback ordering, and iterative refinement critically influ- ence verification success and computational efficiency. 6.2 Traditional Specification Inference Prior to LLMs, specification inference relied on dynamic and static analysis. Tools like Daikon [17] mine invariants from execution traces, while constraint solvers and abstract interpretation meth- ods target lightweight formal properties [6,16]. Some hybrid ap- proaches incorporate symbolic execution or deductive inference [15, 32], though these often operate under constrained grammars or language subsets (e.g., C/Frama-C). Others, like EvoSpex [32], intro- duce ranking or mutation strategies but lack feedback loops from verifiers or adaptive prompt refinement. AutoReSpec departs from these patterns by integrating LLMs with a verifier-guided conversa- tional interface. We introduce a dynamic prompt constructor that adapts based on failure type and validator output, addressing a limitation of prior static and batch-mode approaches. This makes AutoReSpec uniquely suited for open-ended code with real-world variability. 6.3 Evaluation Frameworks and Benchmarks SpecGen [28] and FormalBench [24] offer valuable foundations for evaluating LLM-generated specifications. SpecGen primarily measures verification accuracy under few-shot prompting, while FormalBench’s toolkit broadens the scope to reasoning metrics such as consistency, completeness, and robustness across diverse prompt- ing strategies. However, these frameworks focus on single-model settings and fixed prompts, providing limited insight into how mod- els recover from verification failures, adapt across iterations, or balance accuracy and efficiency. Recent agent-based evaluation ef- forts, such as CodeVisionary [36] and RepoMasterEval [39], further emphasize collaborative judging and mutation-driven analysis for general code-generation tasks. Building on these directions, our benchmark integrates real-world GitHub issue programs and loop- intensive SV-COMP cases, evaluates multiple prompting modes (zero-shot, few-shot, conversational, and collaborative), and sys- tematically tracks verifier feedback, runtime, and validation effort through OpenJML logs. This design enables a comprehensive as- sessment of both effectiveness and efficiency in formal specification generation. 7 Threats to Validity 7.1 Internal Validity Several factors could influence our findings. The wording and struc- ture of prompts can significantly affect LLM responses. Even minor changes in phrasing or example selection, despite borrowing pat- terns from Xia et al. [40], may lead to different behaviors. Second, our evaluation benchmark includes programs drawn from SpecGen- Bench [28] and SV-COMP, both of which contain open-source sam- ples that may have appeared in the pretraining data of proprietary LLMs. Because the training corpora of these models are not publicly disclosed, indirect exposure through related problems or patterns cannot be completely ruled out. To mitigate this risk, we manually compared the generated specifications against reference oracles and publicly available JML examples, finding no lexical or structural overlaps. In addition, our evaluation focuses on formal verification outcomes, as each specification is validated through OpenJML, so correctness is determined by logical consistency rather than textual similarity. These checks substantially reduce the likelihood that data leakage or memorization materially influenced the reported results. We acknowledge that a definitive leakage analysis would require membership inference or embedding-space similarity test- ing, which we plan to perform in future work to quantify residual exposure. Finally, our completeness measure is based on mutation testing. We employ Equivalent Mutant Suppression (EMS) [23] to identify mutants that do not alter program semantics, but some equivalent variants may still slip through. This artifact can slightly overstate the completeness score. Nonetheless, since all methods in our comparison use the same mutation pipeline, the relative differences remain valid. 7.2 External Validity Our evaluation relies on OpenJML for verifying JML-annotated programs. Like any deductive verifier [5], OpenJML cannot de- cide every proof obligation; there are correct specifications that it either rejects or marks unknown because of underlying solver limitations [3,29]. Despite these verifier limitations, AutoReSpec consistently produced valid, provable results for most test programs, including those borrowed from real-world GitHub issues. Our eval- uation is limited to Java/JML verified with OpenJML; therefore, while AutoReSpec is modular, our results do not yet demonstrate language-agnostic performance beyond this setting. We leave cross- language validation to future work. 8 Conclusion and Future Work We introduced AutoReSpec, a novel collaborative framework for verifiable specification generation that integrates dynamic LLM recommendation with verifier-guided prompt refinement. The sys- tem adjusts to the structure of the input program by selecting an LLM pair and a prompting strategy accordingly. This architecture allows AutoReSpec to generate more accurate and verifiable spec- ifications, even for complex program constructs. Our evaluation of 72 Java programs from benchmark suites and real-world bug reports shows that AutoReSpec improves both verification success and completeness compared to previous tools, while significantly reducing evaluation time. To support adoption and future research, we release AutoReSpec as an open-source framework, including a VS Code extension for interactive use and a public leaderboard for reproducible evaluations on our benchmark. Looking ahead, we plan to extend AutoReSpec to other specification languages (e.g., ACSL, Viper), add lightweight static checks for early filtering, and explore on-the-fly prompt adaptation from verifier feedback. We also aim to scale to multi-module systems and concurrent APIs, revisit model selection as LLMs evolve, and broaden support to non-functional specifications (e.g., fairness, robustness). 9 Data Availability The reproducibility package, evaluation results, the full benchmark, and leaderboard [9] are available in an anonymous repository [12] and we hope it serves as a useful resource for future research in this area. AutoReSpec : A Framework for Generating Specification using Large Language ModelsFORGE ’26, April 12–13, 2026, Rio de Janeiro, Brazil References [1]2025. OpenJML 21-0.8. https://github.com/OpenJML/OpenJML/releases/tag/21- 0.8. [Online; accessed Oct-2025]. [2]2025. OpenJML Repository. https://github.com/OpenJML/OpenJML/tree/master- 21. [Online; accessed Oct-2025]. [3]Parosh Aziz Abdulla and Bengt Jonsson. 1996. Undecidable verification problems for programs with unreliable channels. Information and Computation 130, 1 (1996), 71–90. [4]Toufique Ahmed and Premkumar Devanbu. 2022. Few-shot training llms for project-specific code-summarization. In Proceedings of the 37th IEEE/ACM inter- national conference on automated software engineering. 1–5. [5] Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, et al.2005. The KeY tool: integrating object oriented design and formal verification. Software & Systems Modeling 4 (2005), 32–54. [6]Anoud Alshnakat, Dilian Gurov, Christian Lidström, and Philipp Rümmer. 2020. Constraint-based contract inference for deductive verification. Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY (2020), 149–176. [7]Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Ruzica Piskac, Armando Solar-Lezama, and Em- ina Torlak. 2013. Syntax-Guided Synthesis. In Proceedings of the 2013 Formal Methods in Computer-Aided Design (FMCAD). IEEE, 1–17. doi:10.1109/FMCAD. 2013.6679385 [8] Ragib Shahariar Ayon. 2025. AutoReSpec Algorithm Notation. https://github.com/ autorespec/AutoReSpec/blob/main/Algorithm/Algorithm%20Notation.png. [On- line; accessed Nov-2025]. [9]Ragib Shahariar Ayon. 2025. AutoReSpec Leaderboard. https://autorespec.github. io/AutoReSpecLeaderboard/. [Online; accessed Nov-2025]. [10] Ragib Shahariar Ayon. 2025.AutoReSpec Prompts.https://github.com/ autorespec/AutoReSpec/tree/main/Prompts. [Online; accessed Nov-2025]. [11] Ragib Shahariar Ayon. 2025. AutoReSpec Replication Package. https://github. com/autorespec/AutoReSpec/tree/main/Leaderboard. [Online; accessed Nov- 2025]. [12]Ragib Shahariar Ayon. 2025. AutoReSpec Repository. https://github.com/ autorespec/AutoReSpec. [Online; accessed Nov-2025]. [13]Ragib Shahariar Ayon. 2025. AutoReSpec VS Code Extension. https://github.com/ autorespec/AutoReSpec/tree/main/VS-Code%20Extension. [Online; accessed Nov-2025]. [14]Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al.2020. Language models are few-shot learners. Advances in neural information processing systems 33 (2020), 1877–1901. [15]Saikat Chakraborty, Shuvendu K Lahiri, Sarah Fakhoury, Madanlal Musuvathi, Akash Lal, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, and Nikhil Swamy. 2023. Ranking llm-generated loop invariants for program verification. arXiv preprint arXiv:2310.09342 (2023). [16] Patrick Cousot, Radhia Cousot, Manuel Fähndrich, and Francesco Logozzo. 2013. Automatic inference of necessary preconditions. In International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 128–148. [17]Michael D Ernst, Jeff H Perkins, Philip J Guo, Stephen McCamant, Carlos Pacheco, Matthew S Tschantz, and Chen Xiao. 2007. The Daikon system for dynamic detection of likely invariants. Science of computer programming 69, 1-3 (2007), 35–45. [18]Cormac Flanagan, Gary Leavens, K. Rustan M. Leino, and Erik Poll. 2002. JML: Notation for Detailed Design. In Behavioral Specifications of Businesses and Systems (2002), 175–188. doi:10.1007/978-1-4615-0881-8_12 [19]Cormac Flanagan and K Rustan M Leino. 2001. Houdini, an annotation assistant for ESC/Java. In International Symposium of Formal Methods Europe. Springer, 500–517. [20]Xinyi Hou, Yanjie Zhao, Yue Liu, Zhou Yang, Kailong Wang, Li Li, Xiapu Luo, David Lo, John Grundy, and Haoyu Wang. 2024. Large language models for software engineering: A systematic literature review. ACM Transactions on Software Engineering and Methodology 33, 8 (2024), 1–79. [21]Ziwei Ji, Tiezheng Yu, Yan Xu, Nayeon Lee, Etsuko Ishii, and Pascale Fung. 2023. Towards Mitigating LLM Hallucination via Self Reflection. In Findings of the Association for Computational Linguistics: EMNLP 2023, Houda Bouamor, Juan Pino, and Kalika Bali (Eds.). Association for Computational Linguistics, Singapore, 1827–1843. doi:10.18653/v1/2023.findings-emnlp.123 [22]René Just. 2014. The Major mutation framework: Efficient and scalable mutation analysis for Java. In Proceedings of the 2014 international symposium on software testing and analysis. 433–436. [23] Benjamin Kushigian, Samuel J Kaufman, Ryan Featherman, Hannah Potter, Ardi Madadi, and René Just. 2024. Equivalent Mutants in the Wild: Identifying and Efficiently Suppressing Equivalent Mutants for Java Programs. In Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis. 654–665. [24]Thanh Le-Cong, Bach Le, and Toby Murray. 2025. Can LLMs Reason About Pro- gram Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference. (2025). https://openreview.net/forum?id=zXyiakJYzB [25]Thanh Le-Cong, Bach Le, and Toby Murray. 2025. Can LLMs Reason About Pro- gram Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference. arXiv preprint arXiv:2503.04779 (2025). [26]Gary T. Leavens, Albert L. Baker, and Clyde Ruby. 2006. JML: Notation for Detailed Design. In Behavioral Specifications of Businesses and Systems. Springer, Berlin, Heidelberg, 175–188. doi:10.1007/978-3-540-31145-5_12 [27]Liqiang Lu, Yicheng Jin, Hangrui Bi, Zizhang Luo, Peng Li, Tao Wang, and Yun Liang. 2021. Sanger: A Co-Design Framework for Enabling Sparse Attention using Reconfigurable Architecture. In MICRO-54: 54th Annual IEEE/ACM International Symposium on Microarchitecture (Virtual Event, Greece) (MICRO ’21). Association for Computing Machinery, New York, NY, USA, 977–991. doi:10.1145/3466752. 3480125 [28]Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2025. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. In 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). 16–28. doi:10.1109/ICSE55347.2025.00129 [29]Umang Mathur, P Madhusudan, and Mahesh Viswanathan. 2020. What’s de- cidable about program verification modulo axioms?. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 158–177. [30]Quinn McNemar. 1947. Note on the sampling error of the difference between correlated proportions or percentages. Psychometrika 12, 2 (1947), 153–157. [31]Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, and James Noble. 2024. To- wards AI-Assisted Synthesis of Verified Dafny Methods. Proc. ACM Softw. Eng. 1, FSE, Article 37 (July 2024), 24 pages. doi:10.1145/3643763 [32] Facundo Molina, Pablo Ponzio, Nazareno Aguirre, and Marcelo Frias. 2021. EvoSpex: An evolutionary algorithm for learning postconditions. In 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE). IEEE, 1223–1235. [33]Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida, Carroll Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, et al.2022. Training language models to follow instructions with human feedback. Advances in neural information processing systems 35 (2022), 27730–27744. [34]Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. 2023. Can large language models reason about program invariants?. In International Conference on Machine Learning. PMLR, 27496–27520. [35]sosy lab. 2024. SV-COMP - International Competition on Software Verification. https://sites.google.com/view/specgen. [36]Xinchen Wang, Pengfei Gao, Chao Peng, Ruida Hu, and Cuiyun Gao. 2025. Code- Visionary: An Agent-based Framework for Evaluating Large Language Models in Code Generation. arXiv:2504.13472 [cs.SE] https://arxiv.org/abs/2504.13472 [37] Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, and Cong Tian. 2024. Enchanting program specification synthesis by large language models using static analysis and program verification. arXiv preprint arXiv:2404.00762 (2024). [38]Frank Wilcoxon. 1945. Individual comparisons by ranking methods. Biometrics bulletin 1, 6 (1945), 80–83. [39]Qinyun Wu, Chao Peng, Pengfei Gao, Ruida Hu, Haoyu Gan, Bo Jiang, Jinhe Tang, Zhiwen Deng, Zhanming Guan, Cuiyun Gao, et al.2024. Repomastereval: Evalu- ating code completion via real-world repositories. arXiv preprint arXiv:2408.03519 (2024). [40]Chunqiu Steven Xia and Lingming Zhang. 2024. Automated program repair via conversation: Fixing 162 out of 337 bugs for $0.42 each using ChatGPT. In Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis. 819–831. [41]Xiaofei Xie, Bihuan Chen, Liang Zou, Yang Liu, Wei Le, and Xiaohong Li. 2017. Automatic loop summarization via path dependency analysis. IEEE Transactions on Software Engineering 45, 6 (2017), 537–557. [42]Zhengran Zeng, Hanzhuo Tan, Haotian Zhang, Jing Li, Yuqun Zhang, and Ling- ming Zhang. 2022. An extensive study on pre-trained models for program under- standing and generation. In Proceedings of the 31st ACM SIGSOFT international symposium on software testing and analysis. 39–51. [43]Yue Zhang, Yafu Li, Leyang Cui, Deng Cai, Lemao Liu, Tingchen Fu, Xinting Huang, Enbo Zhao, Yu Zhang, Yulong Chen, et al.2023. Siren’s song in the AI ocean: a survey on hallucination in large language models. arXiv preprint arXiv:2309.01219 (2023).