arXiv CSopen access

From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification

1

From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification

arXiv:2604.22601v1 [cs.SE] 24 Apr 2026

Md Erfan, Md Kamal Hossain Chowdhury, Ahmed Ryan, and Md Rayhanur Rahman†

Abstract—Large Language Models (LLMs) show promise in automated software engineering, yet their guarantee of correctness is frequently undermined by erroneous or hallucinated code. To enforce model honesty, formal verification requires LLMs to synthesize implementation logic alongside formal specifications that are subsequently proven correct by a mathematical verifier. However, the transition from informal natural language to precise formal specification remains an arduous task. Our work addresses this by providing the NaturalLanguage2VerifiedCode (NL2VC)-60 dataset: a collection of 60 complex algorithmic problems. We evaluate 11 randomly selected problem sets across seven open-weight LLMs using a tiered prompting strategy: contextless prompts, signature prompts providing structural anchors, and self-healing prompts utilizing iterative feedback from the Dafny verifier. To address vacuous verification, where models satisfy verifiers with trivial specifications, we integrate the uDebug platform to ensure functional validation. Our results show that while contextless prompting leads to near-universal failure, structural signatures and iterative self-healing facilitate a dramatic performance turnaround. Specifically, Gemma 4-31B achieved a 90.91% verification success rate, while GPT-OSS 120B rose from zero to 81.82% success with signature-guided feedback. These findings indicate that formal verification is now attainable for open-weight LLMs, which serve as effective apprentices for synthesizing complex annotations and facilitating high-assurance software development. Index Terms—Formal Verification, Dafny, Program Synthesis, Software Correctness, uDebug

I. INTRODUCTION Formal specifications are indispensable for rigorously defining program logic and facilitating automated reasoning about software correctness. Formal specifications transform ambiguous behaviors into precise semantics, creating a framework for quality assurance through procedure contracts, loop invariants, and assertions. As a result of this mathematical clarity, these specifications have become essential across diverse tasks ranging from software testing [52] and model checking [65] to full-scale program verification. Formal verification is increasingly adopted to develop high-assurance software by providing mathematical proof that programs strictly satisfy their specifications [70] than Md Erfan, Ahmed Ryan, and Md Rayhanur Rahman are with the Department of Computer Science, The University of Alabama, Tuscaloosa, USA. Email: {merfan, aryan9}@crimson.ua.edu, [email protected] Md Kamal Hossain Chowdhury is with the Alabama Water Institute, The University of Alabama, Tuscaloosa, USA. Email: [email protected] † Corresponding author.

traditional dynamic analysis methods such as testing or fuzzing [21]. Consequently, high-stakes domains, including security-sensitive infrastructure, cryptographic libraries, and autonomous aerospace systems, rely on these rigorous correctness guarantees to prevent critical vulnerabilities and operational disruptions [61]. Despite significant breakthroughs in Satisfiability Modulo Theory (SMT) solvers [11], writing program properties and proofs remains a creative, manual process requiring immense expertise. Developers must manually generate complex annotations, such as loop invariants and ranking functions, to enable automated verification tools to complete a proof. This manual process is tedious and timeconsuming, often exceeding the effort required to write the executable code itself. For example, the verification of the seL4 microkernel project [39] required an eleven-person-year effort [56], while the verified code for CompCert C [45] is more than three times the size of the compiler itself [44]. Concurrent with the evolution of formal methods, the rise of Large Language Model (LLM) based assistants has rapidly transformed modern software development workflows. AIdriven tools such as GitHub Copilot [1], Cursor AI [7], and Amazon Q Developer [6] have accelerated programming tasks through natural language to code translation and intelligent autocompletion. By leveraging massive corpora of source code, these systems synthesize complex snippets from informal descriptions to automate traditional refactoring and implementation workflows. This shift has popularized vibe coding [29], where developers rely on high-level intuition and conversational prompts to iterate on software rather than manual line-by-line implementation [62]. However, the use of LLMs in software synthesis introduces a new set of reliability concerns because, despite their fluency, these systems frequently produce code that is syntactically plausible but semantically incorrect, a phenomenon known as hallucinations. Furthermore, LLMs often exhibit insufficient reasoning capabilities when dealing with complex algorithmic logic and remain susceptible to generating insecure patterns due to adversarial poisoning or inherent biases in their training data [35]. Consequently, the need to ensure the correctness and logical integrity of LLM-generated code has emerged as a fundamental challenge in the software engineering community. The problems necessitate a bridge between the synthesis of AI and the rigorous mathematical certainty of formal verification. Furthermore, software requirements are typically written in natural language, which is often ambiguous and imprecise. Capturing complete specifications from such requirements is

2

difficult, and there is currently a lack of direct mapping from natural language to formal specifications. Several formal verification languages exist in the literature, such as F*, Coq, Lean, and the Java Modeling Language (JML); however, we choose Dafny [42] for our framework due to its unique balance of imperative programming and automated theorem proving. Dafny supports verification via Design by Contract [33] using assertions, preconditions, and postconditions. However, even in Dafny, authoring formal specifications and auxiliary verification assertions remains difficult for developers [59]. This challenge is exacerbated by a limited number of training data; while popular languages like Java and Python have over 5 million repositories on GitHub, the Dafny ecosystem has approximately 779 results [28]. This lack of large-scale data makes Dafny particularly challenging for LLM to synthesize correct code without producing hallucinations. To bridge these gaps, we introduce NL2VC-60: Natural Language 2 Verified Code dataset, a novel benchmark designed to evaluate the synthesis of formally verified code from complex, real-world requirements. We began by handauthoring 60 high-quality Dafny programs to optimize our prompt generation strategies, specifically targeting the nuanced demands of competitive programming problems from the UVa Online Judge [78]. The UVa Online Judge is an online automated judging system for programming problems, hosted by the University of Valladolid. Using this foundation, we evaluate randomly selected 11 distinct problem sets across seven leading open-source LLMs using three specialized prompting techniques. Existing work primarily focuses on small-scale, textbook-style problems supported by limited Dafny datasets and natural language inputs that rarely exceed 50 words. In contrast, our problem set overcomes these constraints by incorporating complex algorithmic challenges that require significantly more detailed specifications and extensive descriptive contexts. Our analysis of the resulting code led to the creation of the first comprehensive dataset of Dafny-specific compilation and verification errors in the literature, providing a unique resource for understanding model failure modes in formal methods. We are the first to integrate uDebug [76] community test suites to ensure rigorous functional correctness. uDebug is a community-driven platform designed for competitive programmers to validate their solutions against high-quality test suites. By combining community-driven testing with SMT-based formal proof, NL2VC-60 offers a new standard for code generation that balances complex natural language requirements with mathematical certainty. The goal of this paper is to advance the frontier of AIassisted NL problem-to-code generation by establishing a robust, Dafny-based formal verification framework that evaluates open-weight LLMs’ ability to translate requirements into provably correct and functionally accurate software. The primary contributions of this work are as follows: •

We conduct the first comprehensive empirical study of open-source LLMs synthesizing verifiable Dafny code from real-world requirements, evaluating seven LLM models across three prompting strategies to establish baseline performance in formal code generation.

We introduce NL2VC-60 dataset, a novel benchmark consisting of 60 hand-authored programs to bridges the gap between simple textbook tasks and the nuanced demands of competitive programming tasks. • We provide the first categorization of Dafny-specific compilation and verification errors in the literature, creating a diagnostic dataset of model failure modes to guide future improvements in the synthesis of formal verification. • We establish a rigorous evaluation pipeline for functional correctness by being the first to integrate extensive uDebug community test suites, ensuring synthesized programs are both formally verified and correct across thousands of real-world edge cases. Ultimately, the synthesis of verified methods remains a vast problem space, and this paper serves as an initial exploration of its potential. While our first two contributions address the endto-end task of synthesizing code from narrative prompts, our third contribution, the systematic categorization of compilation and verification errors, highlights that Large Language Models (LLMs) may be most effective when tackling specific subproblems. These include generating formal specifications from natural language, synthesizing imperative code from existing contracts, or focusing exclusively on the annotation bottleneck by producing loop invariants and termination conditions. Our study results suggest that efforts in LLM-assisted coding should concentrate on generating verifiable programs, and that the combination of open-source models with formal verification techniques provides a cost-effective path toward high-assurance software development. Modern software development requires handling real-world requirements, yet existing literature focuses on small, textbook-style programming and algorithmic problems. However, our study relies on different algorithmic patterns, which fully reflect real-world software requirements. We can reduce this gap; by curating a more representative set of problems from the UVa Online Judge. The remainder of this paper is organized as follows. Section II provides a motivational example. Section III establishes the background on the Dafny language, open-weight LLMs, and the uDebug platform. Section IV reviews relevant literature and existing benchmarks. Section V details our methodology, and Section VI presents our experimental results and a detailed analysis of model failure modes. Section VII discusses the implications of our findings and potential threats to validity in Section VIII. Finally, Section IX concludes the paper. •

II. M OTIVATIONAL E XAMPLE We consider the Magic Formula problem (UVa 11934) [77] to illustrate the gap between traditional competitive programming and formal verification. The task requires counting how many values of a quadratic function f (x) = ax2 + bx + c are divisible by a divisor d within the range 0 ≤ x ≤ L. In a typical software engineering workflow, a developer might rely on sample test cases to verify their logic. However, such an approach is prone to off-by-one errors and boundary case failures that testing alone may not catch. By contrast, formal verification ensures that the counting logic remains correct

3

across all possible integer inputs within the specified bounds, transforming a fragile test-based heuristic into a mathematically guaranteed solution. function Power(x:int, n:int): int requires n >= 0 3 decreases n 4 { 5 if n == 0 then 1 else x * Power(x, n-1) 6 } 1 2

7

method MagicFormula(a:int, b:int, c:int, d:int , l:int) returns (result:int) 9 requires d > 0 && l >= 0 10 // Formal Specification: The result must match the cardinality of the set 11 ensures result == |set x:int | 0 <= x <= l && (a*Power(x,2) + b*x + c) % d == 0| 12 // Boundary Case: Constant functions 13 ensures (a == 0 && b == 0 && c % d == 0) ==> result == l + 1 14 { 15 var x, count := 0, 0; 16 while x <= l 17 invariant 0 <= x <= l + 1 18 decreases l - x 19 { 20 var value := (a*Power(x,2) + (b * x) + c); 21 if value % d == 0 { count := count + 1; } 22 x := x + 1; 23 } 24 result := count; 25 } 8

Listing 1: Dafny implementation (Magic Formula problem) Our research proposes a shift from testing-based validation to formal synthesis. As shown in Listing 1, the Dafny implementation goes beyond the imperative logic of the loop by defining a formal contract. The ensures clause specifies the ground truth using mathematical set cardinality:

A. Dafny: A Verification-Aware Programming Language Dafny [19, 42, 43] is a verification-aware, statically typed programming language originally developed at Microsoft Research [53] and currently supported by the Amazon Automated Reasoning group [22]. Dafny bridges the gap between highlevel programming paradigms, including imperative, functional, and object-oriented styles, and formal mathematical proof. A distinguishing feature of Dafny is its native support for Design by Contract, employing Floyd-Hoare-style [33] verification using preconditions (requires), postconditions (ensures), and loop invariants. To develop a verified program, developers provide formal specifications along with executable code. The Dafny static program verifier then checks the functional correctness of the implementation against these specifications. This is achieved by transforming the code into an intermediate verification representation (Boogie) [41], encoding the conditions into predicate calculus, and invoking the Z3 SMT solver [20] to prove their validity. In recent years, Dafny has been used by industry leaders like Amazon to verify AWS authorization logic [16] and by Intel for hardware encryption libraries [80]. While Dafny ensures that the code does what the developer specifies, the difficulty lies in the specification burden. As illustrated in Listing 1, a simple method to find the value of a quadratic function may require more lines of formal annotations (preconditions, postconditions, and invariants) than actual executable code. Researchers have observed that writing these auxiliary verification annotations remains the primary bottleneck in formal software development [59]. If an LLM can successfully synthesize both the implementation and the proofs required for verification, the code generation could lower the barrier for high-assurance software engineering. B. Large Language Models and Open-Weight Models

The landscape of Large Language Models (LLMs) has shifted from a dominance of proprietary APIs (like GPT-4 and PaLM-2) toward highly capable Open-Weight Models result = |{x ∈ Z | 0 ≤ x ≤ L∧(ax2 +bx+c) ≡ 0 (mod d)}| [17]. Unlike closed models, open-weight models [17] such as (1) Llama 3.3 [31], Qwen 3 [83], Gemma 3 [38], and Gemma This example motivates our work: by utilizing LLMs to 4 [51] allow researchers to host the models locally, providing generate both imperative code and associated formal specifica- full control over parameters, token limits, and data privacy. tions, we can leverage SMT solvers to provide a mathematical Recent advancements in these models have demonguarantee of correctness. This approach effectively eliminates strated that smaller, specialized architectures (e.g., Qwen 3 common algorithmic bugs that persist even after extensive Coder [12]) can rival proprietary models in code generation testing on platforms like UVa Online Judge [2]. and logical reasoning tasks. However, applying these openweight models to verification-aware languages such as Dafny remains an underexplored frontier. Because Dafny code is III. BACKGROUND scarce in public training datasets compared to Python or This section provides the theoretical and technical foun- Java, our research explores whether the reasoning capabilities dations for contextualizing our study of AI-assisted formal inherent in modern open-weight architectures can generalize verification. We first discuss the unique architecture of the to the syntactic and logical requirements of formal verification. Dafny language and the inherent challenges of the specification burden. Then we discuss the current state of open-weight LLMs and the iterative prompt engineering techniques used C. Prompt Engineering and Self-Healing to optimize their reasoning. Finally, we introduce uDebug as Prompt engineering [27, 81] is the systematic process of a validation layer to ensure that formally verified programs crafting inputs to align an LLMs output with a specific remain functionally robust under real-world test cases. technical task [63]. In the context of Dafny, prompts must

4

be engineered to be unambiguous and structured. We employ a tiered approach: starting from Contextless Prompting to establish a baseline, moving to Signature Prompting to provide structural anchors, and finally utilizing Self-Healing Prompting. Self-healing [73] mimics the human developer’s workflow by feeding the Dafny verifier’s error messages back into the LLM, allowing the model to iteratively repair its logic and specifications until verification is achieved. D. uDebug: Beyond Vacuous Verification A critical challenge in LLM-driven formal synthesis is vacuous verification, where a model generates weak or trivial specifications that pass the Dafny verifier but do not actually solve the intended problem. We integrate uDebug [76] into our evaluation pipeline to mitigate the problem. uDebug is a community-driven platform designed for competitive programmers to validate their solutions against high-quality test suites. By providing an accepted output for given inputs, uDebug allows us to perform a dual-layer validation: • Formal Layer: The Dafny verifier proves that the code is logically consistent with its formal specifications. • Functional Layer: uDebug ensures the code is semantically correct by testing the generated code against extreme edge cases and boundary conditions contributed by the competitive programming community. As noted by Professor Miguel Angel Revilla (Creator of UVa Online Judge), uDebug is a perfect complement for identifying critical inputs that break solutions [76]. In this research, we use uDebug to confirm that our synthesized, verified Dafny programs are also functionally robust in realworld scenarios type requirements. IV. S UMMARY OF THE L ITERATURE This section contextualizes our research within the broader landscape of automated software engineering and formal verification. We review existing efforts in program synthesis, evaluate the evolving role of LLMs in formal methods, and compare current Dafny-centric benchmarks.

B. LLMs for Formal Methods and Software Engineering LLMs have been increasingly applied to automated proof synthesis and theorem proving, with models like Baldur [24] and Thor [36] outperforming traditional heuristic tools like CoqHammer [18]. Beyond proofs, researchers have utilized LLMs to translate natural language into Isabelle/HOL [82] and event graphs [50]. While general-purpose models like GPT4 often struggle with algorithmic reasoning [25], specialized models such as Minerva [46, 57] demonstrate that domainspecific pre-training can mitigate these limitations. In the broader software engineering context, LLMs now support code completion, repair, and test generation [58, 75]. Our research follows the philosophy of letting LLMs generate plausible candidates while leveraging the Dafny verifier to guarantee correctness, effectively filtering out the hallucinations common in LLM-generated code. C. Benchmarking Dafny Generation Existing literature on LLM-based Dafny generation remains relatively limited in both dataset scale, limited word length for problems, and problem diversity. Prior studies have primarily evaluated models ranging from GPT-3.5 to the recent Llama 3.3 [31], Qwen 3 [83], and Gemma 3 [67] on a narrow set of benchmarks. Table I provides a comparative overview with limitations of existing literature. As shown in the table, benchmarks like Clover [69] and MBPP-Dafny [8] focus on textbook-level tasks with average lengths of only on average 19 lines of code. DafnyBench [48] represents a greater effort with 782 samples, yet the research relies heavily on converted rather than native requirements. Besides that, existing work primarily focuses on small-scale, textbook-style problems supported by limited Dafny datasets and natural language inputs that rarely exceed 50 words. In contrast, our problem set overcomes these constraints by incorporating complex algorithmic challenges that require significantly more detailed specifications and extensive descriptive contexts. While frameworks like ATLAS [9] synthesize verified code using algorithmic references and test cases, our approach targets the direct synthesis of Dafny programs from NL descriptions, addressing the complexity of requirements.

A. Program Synthesis and Verification with Dafny In the last two decades, formal methods for software synthesis [32] and verification [64] have transitioned from esoteric research topics to practical industrial tools [37, 42]. Modern tools like Dafny, SAW, and SPIN are now mature enough to support critical applications in encryption algorithms [84], Ethereum Virtual Machine (EVM) bytecodes [13], scientific software, and quantum circuitry [47]. Despite this maturity, a barrier to adoption remains the scarcity of engineers trained in formal specification [26]. The gap has spurred research into automated support for Dafny, such as XDsmith for differential testing [34] and techniques for generating counterexamples when verifiers fail [14]. Our work builds on this momentum by exploring how LLMs can bridge the gap between Natural Language (NL) requirements and verified Dafny code.

V. A PPROACH This study aims to bridge the gap between textbook-style benchmarks and real-world software requirements by evaluating LLM performance on complex algorithmic tasks curated from the UVa Online Judge. We focus on the transition from NL requirements to formally verified Dafny code through tiered prompting and iterative repair. A. Research Questions We investigate the capability of LLMs to synthesize formally verified Dafny methods. We employ a tiered evaluation strategy to isolate the impact of structural hints and iterative feedback. We address the following research questions: RQ1- (Contextless Prompting): How effective are LLMs at synthesizing fully verified Dafny methods when provided

5

TABLE I: Comparison of Dafny Verification Datasets and Benchmarks Work / Dataset Clover [69] MBPP-Dafny [8] HumanEval-Dafny [10] DafnyBench [48]

Input Type Short NL / Ann. NL (short) NL (short) Mixed

Problem Type Textbook Basic Python Algorithmic Real + Textbook

Dafny Yes Yes Yes Yes

Size 63–66 164 132 782

Avg Code ∼19 LoC ∼19 LoC ∼50 LoC ∼53 LoC

TacoDafny [79] ATLAS [9] SpecGen [49]

NL (Gen.) Alg. + Ref. NL

Synthetic Algorithmic LeetCode

Yes Yes No

Auto. Large N/A

Varies Varies N/A

only with a natural language description, without any formal structural hints? RQ2- (Signature Prompting): How does the provision of a formal method signature and accompanying functional tests affect the initial synthesis success rate compared to contextless prompting? RQ3- (Self-Healing Capabilities): To what extent can an iterative feedback loop recover failed synthesis attempts under varying initial conditions? RQ3a (Self-Healing with Contextless Prompting): Can LLMs repair verification failures when the initial attempt was generated from NL alone? RQ3b (Self-Healing with Method Signature): Does the presence of a pre-defined method signature provide a superior result for the self-healing process, leading to higher repair rates than contextless healing? RQ4- (Error Analysis ): To what extent can error descriptions help to overcome errors by using the signature prompt and the self-healing method? B. Problem Curation and Abstraction This subsection details the systematic process of converting competitive programming tasks into standardized formal requirements to ensure high-fidelity evaluation of LLM. 1) Test Dataset: We conducted our study using a collection of problems with rich natural-language descriptions and corresponding formally verified Dafny code. Existing literature often relies on small-scale, textbook-style datasets like MBPP or HumanEval; however, these focus on basic programming tasks with short specifications. To evaluate LLMs on complex, real-world requirements, we curated 60 set of problems from the UVa Online Judge, an automated judging system with thousands of competitive programming problems [2]. 2) Problems Generalization: Unlike benchmarks that use one-line descriptions, UVa problems provide paragraph-level specifications involving different programming tasks, with average word counts exceeding 179. However, these problems are typically encumbered by what we term presentation flavor details designed for contest environments (e.g., input formatting, multiple test case counts like |t| < 15, and arbitrary constraints like |a| < 109 ) that do not contribute to the semantic understanding of the requirement. To adapt these for formal verification, we performed a Generalization Process in Table II to make the problems generic. We manually transformed the competitive programming descriptions into a more generic, requirement-focused form by

Limitations Simple problems, small scale Entry-level tasks only Still benchmark-style Limited human-written verified programs Synthetic, not real-world No direct NL to Dafny Uses OpenJML, not Dafny

removing presentation-specific instructions while preserving the core computational logic. For example, a problem asking to identify relational operators (“>”, “<”, or “=”) between two integers was stripped of its “process T lines” loop instructions and reduced to its functional essence. 3) Empirical Problem Selection: We selected 60 problems based on their acceptance rates and user submission statistics to act as a proxy for practical relevance. Across the selected problems, total submissions varied from approximately 27,000 to over 370,000 in the online Judge platform, ensuring the tasks were neither trivial nor excessively niche. For each generalized problem, we developed ground-truth Dafny verification code by all the authors to ensure a unified and satisfactory implementation standard. We utilized the uDebug platform to access a diverse collection of test cases, including edge and corner cases, to validate the functional correctness of our verified solutions. This resulted in our main test dataset, NL2VC-60: a collection of 60 real-world algorithmic problems, each consisting of a generic requirement description, a formal method signature, and a suite of validation test cases. Since no public Dafny implementations of UVa problems existed prior to this study, our dataset minimizes the risk of data leakage during LLM evaluation. C. Human Written Dataset: NL2VC-60 To perform Dynamic Few-Shot Prompting, we required a high-quality, diverse collection of verified Dafny methods to serve as in-context exemplars. Given the absence of existing datasets that map complex natural language requirements to Dafny, we manually developed a reference set, NL2VC-60, consisting of 60 problems from our suite. This process involved translating the core computational requirements of 60 UVa problems into complete Dafny implementations. Unlike standard coding tasks, this required the manual formulation of formal specifications, including method preconditions (requires), postconditions (ensures), and complex loop invariants until the Dafny verifier could formally prove the code’s correctness. We performed all necessary annotations, hint insertions, and structural refinements until the verifier signaled a successful proof for each method. In developing this dataset, we experienced first-hand the significant cognitive load associated with formal specification. Formulating precise postconditions that capture the semantic intent of paragraph-level requirements and providing sufficient invariants for algorithmic logic proved to be a rigorous undertaking. The creation took approximately 300 person-hours for the authors and 50 more hours to resolve conflicts among

6

TABLE II: Comparison Between Original UVa Problem Description and Generalized Generic Description Component

Original UVa Problem Description (Competitive Flavor)

Generic Description (Requirement Focused)

Description

Some operators checks about the relationship between two values and these operators are called relational operators. Given two numerical values your job is just to find out the relationship between them that is (i) First one is greater than the second (ii) First one is less than the second or (iii) First and second one is equal.

Some operators checks about the relationship between two values and these operators are called relational operators. Given two numerical values your job is just to find out the relationship between them that is (i) First one is greater than the second (ii) First one is less than the second or (iii) First and second one is equal.

Input

First line of the input file is an integer t (t < 15) which denotes how many sets of inputs are there. Each of the next t lines contain two integers a and b (|a|, |b| < 1000000001).

The input contain two integers a and b.

Output

For each line of input produce one line of output. This line contains any one of the relational operators ’>’, ’<’ or ’=’, which indicates the relation that is appropriate for the given two numbers.

The output contains any one of the relational operators ’>’, ’<’ or ’=’, which indicates the relation that is appropriate for the given two numbers.

Sample Input

3 10 20 20 10 10 10

10 20 20 10 10 10

Sample Output

< > =

< > =

authors to create this dataset of 60 formally verified problems, even with access to official Dafny documentation [72]. D. Functional Validation via uDebug A significant limitation in existing formal synthesis literature is the reliance on simplified functional validation. Current benchmarks typically employ either a small set of basic inputoutput pairs [55] or rely on the LLM itself to generate test cases [79]. Such methods often fail to identify subtle semantic bugs because they rarely cover the complex edge and corner cases inherent to algorithmic problems. To address this gap, we incorporate uDebug [76] into our validation pipeline for the first time in the context of Dafny synthesis. uDebug is a community-driven platform that provides extensive, high-quality test suites for competitive programming problems, specifically designed to uncover logical flaws through extreme inputs and boundary conditions. We ensure a dual-layer validation process by using uDebug: while the Dafny verifier proves that the code satisfies its formal specification, the uDebug integration confirms that the code remains functionally correct across a comprehensive range of real-world scenarios. This approach eliminates the circularity of using an LLM to test its own generated code and provides a much higher degree of confidence in the programs’ robustness than standard textbook-style test sets.

selected a diverse suite of contemporary LLMs ranging from 4B to 176B parameters, including both general-purpose and code-specialized architectures. To evaluate the performance of diverse generative architectures on formal Dafny synthesis, we utilize a selection of seven state-of-the-art Large Language Models (LLMs) ranging from specialized coding assistants to massive-scale general reasoners. Our general-purpose reasoning suite includes GPTOSS-120B [60], GPT-OSS-20B [60], and Gemma 4-31b [30], which provide a baseline for high-level logic and instruction following. These are contrasted with a series of models specifically optimized for software engineering tasks: Qwen3.59B [5], Qwen3-Coder-30B [4], Codestral-22b-v0.1 [54], and the mixture-of-experts (MoE) based Qwen3.6-35b-a3b [4]. By evaluating models across this spectrum of parameter sizes and training objectives, we can analyze the correlation between general reasoning capacity and the precision required for formal specification generation. Table III provides a detailed overview of the model suite. Each model was evaluated across five temperature settings (T = 0.0 to 0.8) to identify the optimal configuration for balancing creative exploration with logical precision. We consider the open-source weights architectures; our study provides a comprehensive look at the current state of automated formal verification across different scales of machine intelligence.

E. LLM Selection and Evaluation Setup

F. Prompt Design

Program synthesis in a verification-aware language like Dafny requires more than syntactic fluency. The synthesis demands an intricate understanding of formal semantics, proof obligations, and the underlying theorem-proving logic of the language [24]. To evaluate these reasoning capabilities, we

Based on our research questions and the unique challenges posed by the NL2VC-60 dataset, we designed three distinct prompting strategies. Each level of prompting is intended to evaluate how increasing structural context and iterative feedback affect the synthesis of verified Dafny programs.

7

TABLE III: Large Language Models Evaluated for Dafny Synthesis Model

Params

Context

Type

Category

GPT-OSS-120B Qwen 3.6-35B-A3B Gemma 4-31B Qwen 3 Coder 30B Codestral-22B-v0.1 GPT-OSS-20B Qwen 3.5-9B

120B 35B 31B 30B 22B 20B 9B

131k 256k 256k 160k 32k 128k 262k

OS OS OS OS OS OS OS

General Agentic Multimodal Coder Coder General General

OS = Open-Source Weights

1) RQ1 [Contextless Prompting]: To answer RQ1, we use contextless prompting by providing only the natural language problem description without any additional structural guidance. This setup establishes a baseline to evaluate the model’s ability to infer program structure, formal specifications, and verification constraints (such as termination arguments) directly from the requirement. Contextless Prompt: You are an expert in Dafny. Output ONLY raw Dafny code. Generate one Dafny source file for the following task. Problem ID: <Problem_ID> Task Description: <Generalized_Description>

2) RQ2 [Method Signature Prompting]: For RQ2, we utilize method signature prompting by supplying an additional structured hint in the form of a formal method signature. This guidance constrains the solution space and helps the model align its implementation with the expected input-output behavior and type-system requirements. Code generation experiments for non-verified code often perform better when prompted with signatures; we hypothesize that this formal frame is even more critical for successful verification in Dafny. Method Signature Prompt: You are an expert in Dafny. Output ONLY raw Dafny code. Generate one Dafny source file for the following task. Problem ID: <Problem_ID> Task Description: <Generalized_Description> Method Signature Prompt: <Method_Signature_Prompt>

3) RQ3 [Self-Healing Prompting]: To address RQ3, we employ self-healing prompting by iteratively refining generated programs based on direct feedback from the Dafny verifier. When a generated program fails verification, we feed the specific error messages (e.g., assertion violations or termination failures) back into the model along with the previous code. We apply this process to both contextless and method-signature settings (RQ3a and RQ3b) to evaluate the model’s capacity to correct specification errors and invariant issues through autonomous repair. Self-Healing Prompt: The previous Dafny code failed verification with the following errors: <Dafny_Verifier_Output> Please repair the code to satisfy all specifications. Output ONLY the raw fixed Dafny code.

G. Evaluation Metrics We evaluate the quality of the LLM-synthesized methods using a multi-layered approach that combines formal verification, functional validation, and qualitative error analysis. 1) Quantitative Metrics: verify@k and functional@k: The primary metric for our study is verify@k (adapted from pass@k [15, 40]), which measures the model’s ability to produce at least one formally verified solution within k attempts. A problem is considered solved under this metric only if the Dafny verifier signals that the implementation satisfies all formal specifications, as follows in existing research [55]. 2) Qualitative Assessment: Specification Strength and Error Analysis: Automated metrics serve as a proxy for performance, but they do not capture the nuance of formal reasoning. To assess the semantic depth of the results, we manually reviewed all verified methods to ensure they contain strong formal specifications, specifically, postconditions that fully capture the problem’s requirements rather than assertions. For the failures observed in RQ3 (Self-Healing), we conducted a manual inspection of the verifier’s error logs. We categorized these failures into distinct types, such as termination failures (missing or incorrect decreases clauses), invariant violations, and index out-of-bounds errors. This analysis allows to evaluate the extent to which the iterative feedback loop addresses the logical challenges of formal proof development. H. Temperature Tuning The temperature is a hyperparameter in LLMs that controls the randomness and creativity of the decoding process [3, 66, 74]. Lower temperatures lead to more deterministic and focused outputs, while higher temperatures encourage diversity at the risk of logical incoherence. Since formal synthesis in Dafny requires high structural precision, identifying the optimal temperature for maximizing verification rates. To determine the ideal configuration for our study, we conducted a temperature tuning experiment on a subset of the NL2VC-60 dataset. We selected a representative sample of problems and executed each across five distinct temperature settings: T ∈ {0.0, 0.2, 0.4, 0.6, 0.8}. This range allows us to observe the transition from greedy decoding (T = 0.0) to high-variance sampling (T = 0.8). We evaluated the synthesized methods using the verify@k metric where k ∈ {1, 3, 5}. Our preliminary results indicated that lower temperatures (0.0 to 0.4) generally yielded higher success rates for initial synthesis (RQ1 and RQ2), as the models remained more faithful to Dafny’s strict syntax. However, for the Self-Healing process (RQ3), slightly higher temperatures occasionally proved beneficial by allowing the model to explore alternative algorithmic implementations when the primary logic failed to verify. Based on these findings, we report our final results using the optimal temperature identified for each specific model and prompt type. I. Error Analysis We analyzed the error logs for different methods on identified three types of errors. We then examined the error types and classified them into several subgroups. Table VII demonstrates the presence of different types of errors in open source LLMs.

8

1) Syntax Errors: Dominant in Contextless and Signature Prompting for most models. This confirms that without iterative feedback, models frequently struggle with Dafny’s specific grammar (e.g., missing semicolons, improper loop syntax). 2) Semantic / Type Errors: High in models like GPT-OSS120B and MistralAI. These occur when the code is structurally correct but violates Dafny’s strict type system, or attempts to use unavailable modules (such as System). 3) Verification Errors: Notably higher in Self-Healing categories for models like Gemma 4 and Qwen3-Code30B. This suggests that as models fix their syntax through iterations, they reach a stage where the code compiles but fails the deeper logical proof (e.g., an assertion might not hold). J. Experimental Setup To conduct our large-scale synthesis and verification experiments, we utilized a distributed environment comprising a high-performance inference server and a local development machine. For the open-source Large Language Models (LLMs), we deployed LM Studio version 0.4.8 (Build 1) on a dedicated Ubuntu-based server. This server features a high-end hardware configuration equipped with four NVIDIA RTX 6000 Ada Generation GPUs, each providing 48 GB of VRAM (totaling 192 GB), supported by NVIDIA Driver version 580.126.09 and CUDA 13.0. This infrastructure allowed us to host and query large-parameter models locally, ensuring consistent inference latency for our 60-problem dataset. For the development of orchestration scripts and the formal verification of synthesized methods, we used a MacBook Pro (Model Mac16,8) running macOS 15.3.1. The software environment was managed using Visual Studio Code version 1.115.0 (arm64) and Python 3.14.4 within a dedicated virtual environment in our experiments. To manage the iterative repair process, our self-healing orchestration script was configured with a maximum of 10 repair attempts per problem. If a model failed to produce a verified solution within these ten iterations, the result was recorded as a failure for that specific trial. Furthermore, to accommodate the processing time of large models (such as GPT-OSS-120B) and prevent connection timeouts, we implemented a response wait time of 180 seconds for all LM Studio API calls during our experiments. For verifying the code, we employed Dafny 4.11.0 [71], which represents a modern and stable iteration of the language. Since recent versions of Dafny introduced significant changes to the verification engine and syntax compared to the 3.x series, our experiments provide a rigorous test of the models’ ability to adapt to contemporary formal verification standards. All functional validation against uDebug [76] test suites was executed within this same environment to ensure parity between the formal proof and the executable implementation. VI. R ESULTS This section presents the empirical findings of our study. To establish a robust evaluation framework, we manually developed NL2VC-60, a benchmark dataset consisting of 60 formally verified Dafny programs used to optimize our tiered

prompting strategies. For the primary comparative analysis, we evaluated seven state-of-the-art open-weight models against a subset of randomly selected 11 algorithmic problems. Performance is measured using the verif y@k metric, indicating the percentage of problems for which at least one successful verification was achieved within k attempts. A. RQ1: Performance of Contextless Prompting The initial evaluation of LLMs using contextless prompting shows significant disparities in their ability to synthesize verifiable Dafny code from raw requirements. As shown in Table IV, the majority of the tested models, including the massive GPT OSS 120B and the Qwen series, failed to produce a single verified solution across all temperature settings. This widespread failure suggests that simply providing a natural language problem description is insufficient for most models to navigate the syntactic and semantics of the Dafny language. Several observations emerge from the RQ1: • Unlike the other general purpose models, Gemma 4-31B showed a surprising aptitude for generating verifiable programs even without external context. The model achieved a peak verify@5 success rate of 54.55% at a temperature of 0.2. This performance indicates that its pretraining likely involved a higher density of formal or algorithmic logic, allowing it to guess correct loop invariants and post-conditions that other models completely missed. • Codestral was the only other model to consistently yield results, reaching a peak verify@5 of 27.27% at T = 0.8. The success of this model at higher temperatures suggests that while the model possesses the basic syntactic intuition for Dafny. The model often requires more stochastic exploration to arrive at the precise formal annotations needed to satisfy the Z3 SMT solver. • The 0% success rate of the remaining five models highlights a fundamental challenge in the field. Even highly capable models struggle to infer complex formal specifications from scratch. The findings are reinforcing the need for more structured prompting techniques or retrieval augmentation to bridge the gap between informal requirements and mathematical proof. B. RQ2: Performance of Signature Prompting The second phase of our evaluation explores the impact of providing the method signature as additional context. As illustrated in Table V, the structural guidance resulted in a performance shift, effectively reversing the widespread failures observed in the contextless setting. By providing the skeleton of the Dafny method including the input parameters and return types, the models were freed from the burden of syntactic structure and could instead focus on synthesizing the internal logic and required verification annotations. Several observations emerge from the RQ2: • The most striking improvement was observed in GPTOSS-120B. While this model recorded a 0% success rate in RQ1, the introduction of method signatures allowed it to achieve a peak verify@5 rate of 63.64% at T = 0.8.

9

TABLE IV: Complete Verification Success Rates for Contextless Prompting (RQ1) Model

Temp (T)

verify@1

verify@3

verify@5

Succ.

Total

%

Succ.

Total

%

Succ.

Total

%

GPT-OSS-120B

0.0 0.2 0.4 0.6 0.8

0 0 0 0 0

11 11 11 11 11

0.00% 0.00% 0.00% 0.00% 0.00%

0 0 0 0 0

11 11 11 11 11

0.00% 0.00% 0.00% 0.00% 0.00%

0 0 0 0 0

11 11 11 11 11

0.00% 0.00% 0.00% 0.00% 0.00%

Qwen 3.5-9B

0.0 0.2 0.4 0.6 0.8

0 0 0 0 0

11 11 11 11 11

0.00% 0.00% 0.00% 0.00% 0.00%

0 0 0 0 0

11 11 11 11 11

0.00% 0.00% 0.00% 0.00% 0.00%

0 0 0 0 0

11 11 11 11 11

0.00% 0.00% 0.00% 0.00% 0.00%

Qwen 3 Coder 30B

0.0 0.2 0.4 0.6 0.8

0 0 0 0 0

11 11 11 11 11

0.00% 0.00% 0.00% 0.00% 0.00%

0 0 0 0 0

11 11 11 11 11

0.00% 0.00% 0.00% 0.00% 0.00%

0 0 0 0 0

11 11 11 11 11

0.00% 0.00% 0.00% 0.00% 0.00%

GPT-OSS 20B

0.0 0.2 0.4 0.6 0.8

0 0 0 0 0

11 11 11 11 11

0.00% 0.00% 0.00% 0.00% 0.00%

0 0 0 0 0

11 11 11 11 11

0.00% 0.00% 0.00% 0.00% 0.00%

0 0 0 0 0

11 11 11 11 11

0.00% 0.00% 0.00% 0.00% 0.00%

Codestral-22B

0.0 0.2 0.4 0.6 0.8

1 1 1 1 1

11 11 11 11 11

9.09% 9.09% 9.09% 9.09% 9.09%

1 1 2 2 1

11 11 11 11 11

9.09% 9.09% 18.18% 18.18% 9.09%

1 2 2 1 3

11 11 11 11 11

9.09% 18.18% 18.18% 9.09% 27.27%

Qwen 3.6-35B

0.0 0.2 0.4 0.6 0.8

0 0 0 0 0

11 11 11 11 11

0.00% 0.00% 0.00% 0.00% 0.00%

0 1 1 0 0

11 11 11 11 11

0.00% 9.09% 9.09% 0.00% 0.00%

0 2 2 1 1

11 11 11 11 11

0.00% 18.18% 18.18% 9.09% 9.09%

Gemma 4-31B

0.0 0.2 0.4 0.6 0.8

3 0 0 2 2

11 11 11 11 11

27.27% 0.00% 0.00% 18.18% 18.18%

3 4 5 5 3

11 11 11 11 11

27.27% 36.36% 45.45% 45.45% 27.27%

3 6 3 4 4

11 11 11 11 11

27.27% 54.55% 27.27% 36.36% 36.36%

This suggests that the model possesses a deep latent knowledge of formal verification and Dafny logic but lacks the ability to self-structure the initial code container from raw requirements. • Surprisingly, Qwen 3.5-9B emerged as the top performer in this category, reaching a peak verify@5 success rate of 72.73%. This indicates that signature prompting provides constraint to allow smaller models to focus their computational budget on the complex task, often outperforming much larger general-purpose models. • Unlike the zero-shot results, peak performance under signature prompting was consistently achieved at higher temperatures (typically T = 0.8). This suggests that once the structural constraints are fixed via the signature, the models benefit from increased stochastic exploration to identify the precise mathematical formulations. For example, specific loop invariants or termination measures required to satisfy the SMT solver. • All seven models demonstrated signs of life in this setting, with even the weakest models surpassing a 30%

success rate at their peak. This confirms that the primary bottleneck in verifiable code generation is not necessarily the logic itself, but the difficulty of mapping informal natural language to the rigid formal signatures required by the Dafny compiler. C. RQ3: Performance of Self-Healing Mechanisms The third research question evaluates the efficacy of iterative self-healing, where models are provided with error feedback from the Dafny compiler to repair their own code. The evaluation consists of two strategies: healing from a contextless baseline (RQ3a) and healing from a signature-guided baseline (RQ3b). As shown in Table VI, the ability to self-correct varies significantly across models, with the initial prompt quality serving as a critical predictor of repair success. • RQ3a: Contextless Healing: When attempting to heal from the zero-shot failures of RQ1, most models remained stagnant. GPT-OSS-120B and several others continued to post 0% success rates. The findings suggests that

10

TABLE V: Verification Success Rates for Signature Prompting (RQ2) Model

Temp (T)

verify@1

verify@3

verify@5

Succ.

Total

%

Succ.

Total

%

Succ.

Total

%

GPT-OSS-120B

0.0 0.2 0.4 0.6 0.8

6 5 6 6 6

11 11 11 11 11

54.55% 45.45% 54.55% 54.55% 54.55%

6 6 6 5 7

11 11 11 11 11

54.55% 54.55% 54.55% 45.45% 63.64%

6 6 6 6 7

11 11 11 11 11

54.55% 54.55% 54.55% 54.55% 63.64%

Qwen 3.5-9B

0.0 0.2 0.4 0.6 0.8

3 4 2 2 4

11 11 11 11 11

27.27% 36.36% 18.18% 18.18% 36.36%

2 3 5 4 5

11 11 11 11 11

18.18% 27.27% 45.45% 36.36% 45.45%

2 5 4 3 8

11 11 11 11 11

18.18% 45.45% 36.36% 27.27% 72.73%

Qwen 3 Coder 30B

0.0 0.2 0.4 0.6 0.8

3 3 4 4 4

11 11 11 11 11

27.27% 27.27% 36.36% 36.36% 36.36%

4 4 5 4 4

11 11 11 11 11

36.36% 36.36% 45.45% 36.36% 36.36%

3 3 5 5 4

11 11 11 11 11

27.27% 27.27% 45.45% 45.45% 36.36%

GPT-OSS 20B

0.0 0.2 0.4 0.6 0.8

3 4 2 5 2

11 11 11 11 11

27.27% 36.36% 18.18% 45.45% 18.18%

3 5 4 6 6

11 11 11 11 11

27.27% 45.45% 36.36% 54.55% 54.55%

3 5 5 4 5

11 11 11 11 11

27.27% 45.45% 45.45% 36.36% 45.45%

Codestral-22B

0.0 0.2 0.4 0.6 0.8

3 4 3 2 3

11 11 11 11 11

27.27% 36.36% 27.27% 18.18% 27.27%

3 4 2 3 2

11 11 11 11 11

27.27% 36.36% 18.18% 27.27% 18.18%

3 5 5 7 6

11 11 11 11 11

27.27% 45.45% 45.45% 63.64% 54.55%

Qwen 3.6-35B

0.0 0.2 0.4 0.6 0.8

2 2 2 1 0

11 11 11 11 11

18.18% 18.18% 18.18% 9.09% 0.00%

3 3 3 3 3

11 11 11 11 11

27.27% 27.27% 27.27% 27.27% 27.27%

7 3 4 4 3

11 11 11 11 11

63.64% 27.27% 36.36% 36.36% 27.27%

Gemma 4-31B

0.0 0.2 0.4 0.6 0.8

3 3 3 3 5

11 11 11 11 11

27.27% 27.27% 27.27% 27.27% 45.45%

3 3 3 3 7

11 11 11 11 11

27.27% 27.27% 27.27% 27.27% 63.64%

5 6 4 4 7

11 11 11 11 11

45.45% 54.55% 36.36% 36.36% 63.64%

without an initial structural foundation, compiler error messages are too abstract for the model to navigate toward a valid solution. However, Gemma 4-31B proved to be a notable exception, demonstrating a remarkable selfcorrection capability. By leveraging compiler feedback, it achieved a peak verify@5 rate of 90.91% at T = 0.2 and T = 0.6, indicating that it can effectively use error logs to guess missing loop invariants and post-conditions. • RQ3b: Signature-Guided Healing: Self-healing proved most potent when initiated from the signature-guided prompts of RQ2. In this setting, the structural skeleton provided enough stability for the compiler feedback to be actionable. GPT-OSS-120B demonstrated the most significant turnaround, rising to a peak of 81.82% success at T = 0.2. This suggests that when the method signature is fixed, larger models are efficient at using error feedback to refine mathematical proofs and satisfy the SMT solver. • Unlike previous rounds, several models (such as Qwen 3 Coder 30B) reached a plateau where performance remained consistent across temperatures in the signature-

guided setting. Conversely, Gemma 4-31B maintained high performance (over 80%) in both RQ3a and RQ3b, establishing itself as the most robust model for autonomous Dafny development, regardless of the initial prompt’s context level. D. RQ4: Qualitative Error Analysis and Failure Taxonomy We conducted a systematic qualitative analysis of our total runs to understand the specific challenges in automated formal synthesis as depicted in Table VII. We categorized failures into a three-tiered taxonomy: Syntax Errors (malformed code structure), Semantic and Type Errors (type mismatches or API hallucinations), and Verification Failures (syntactically correct code that the SMT solver cannot prove). 1) Syntactic Fragility and Contextual Dependence: Our analysis confirms that syntax errors are the primary bottleneck for models lacking structural anchors. In contextless settings, GPT OSS 20B and GPT OSS 120B produced syntax errors in the majority of attempts. These failures typically

11

TABLE VI: Detailed Verification Success Rates for Self-Healing (RQ3) Model

Temp (T)

Contextless Healing (RQ3a)

Signature-Guided Healing (RQ3b)

Succ.

Total

%

Succ.

Total

%

GPT-OSS-120B

0.0 0.2 0.4 0.6 0.8

0 0 0 0 0

11 11 11 11 11

0.00% 0.00% 0.00% 0.00% 0.00%

7 9 7 8 7

11 11 11 11 11

63.64% 81.82% 63.64% 72.73% 63.64%

Qwen 3.5-9B

0.0 0.2 0.4 0.6 0.8

3 0 2 0 0

11 11 11 11 11

27.27% 0.00% 18.18% 0.00% 0.00%

2 3 5 4 3

11 11 11 11 11

18.18% 27.27% 45.45% 36.36% 27.27%

Qwen 3 Coder 30B

0.0 0.2 0.4 0.6 0.8

2 2 3 1 6

11 11 11 11 11

18.18% 18.18% 27.27% 9.09% 54.55%

6 6 6 6 6

11 11 11 11 11

54.55% 54.55% 54.55% 54.55% 54.55%

GPT-OSS 20B

0.0 0.2 0.4 0.6 0.8

0 1 0 0 1

11 11 11 11 11

0.00% 9.09% 0.00% 0.00% 9.09%

4 4 7 5 4

11 11 11 11 11

36.36% 36.36% 63.64% 45.45% 36.36%

Codestral-22B

0.0 0.2 0.4 0.6 0.8

0 0 0 1 0

11 11 11 11 11

0.00% 0.00% 0.00% 9.09% 0.00%

2 3 5 6 3

11 11 11 11 11

18.18% 27.27% 45.45% 54.55% 27.27%

Qwen 3.6-35B

0.0 0.2 0.4 0.6 0.8

0 0 1 0 2

11 11 11 11 11

0.00% 0.00% 9.09% 0.00% 18.18%

4 4 4 4 6

11 11 11 11 11

36.36% 36.36% 36.36% 36.36% 54.55%

Gemma 4-31B

0.0 0.2 0.4 0.6 0.8

8 10 9 10 8

11 11 11 11 11

72.73% 90.91% 81.82% 90.91% 72.73%

7 7 8 9 9

11 11 11 11 11

63.64% 63.64% 72.73% 81.82% 81.82%

involve the misuse of Dafny-specific keywords or the generation of Pythonic indentation, which is incompatible with Dafny’s curly-brace syntax. This suggests that while openweight models possess general algorithmic logic, they lack the specific syntactic density required for niche-verification languages without external guidance. 2) Semantic Drift and Invariant Generation: As we transitioned to Signature Prompting, syntax errors decreased significantly, but we observed a sharp rise in semantic and type errors. Models frequently hallucinate non existent predicates or attempt to perform arithmetic on incompatible types, such as treating a sequence as a set. A critical finding is the Invariant Gap; even when models generate correct imperative logic, they often fail to provide the inductive loop invariants required for the Z3 solver to complete the proof. Models like Qwen 3 Coder 30B demonstrated a tendency to repeat the same insufficient invariant across multiple self-healing iterations, indicating a logical plateau in the repair process. 3) Functional Robustness and Vacuity: The most complex category involves code that satisfies the verifier but fails

the functional test suite. By integrating uDebug, we identified several instances where models achieved verification by providing weak specifications. For instance, a model might satisfy a postcondition by returning a trivial constant that happens to meet a weak mathematical constraint. The uDebug community test cases acted as a vital truth oracle, identifying these as functional failures and ensuring that the verified code maintains real world utility against extreme edge cases. VII. F INDINGS AND D ISCUSSION This section presents a comprehensive analysis of our experimental results, detailing how different architectural scales and prompting methodologies influence the synthesis of provably correct code. By systematically decomposing the performance of seven state-of-the-art models across four Research Questions (RQs), we illustrate the critical transition from natural language requirements to formal mathematical proofs. The following findings highlight the interplay between model reasoning, structural guidance, and the iterative feedback loops required to overcome the data-scarcity bottleneck in the Dafny.

12

TABLE VII: Dafny Compilation and Verification Errors Model

Prompt Strategy Total Runs

Syntax Errors

Semantic/Type Errors

Verification

Verified

GPT-OSS-120B

Contextless Signature Prompt Self-Healing

564 816 1,134

435 397 620

45 53 471

0 111 5

0 150 20

GPT-OSS-20B

Contextless Signature Prompt Self-Healing

672 816 1,564

597 397 793

75 53 149

0 111 166

0 150 395

Codestral-22B

Contextless Signature Prompt Self-Healing

1,285 792 1,666

732 407 1,116

518 217 188

0 0 58

33 138 217

Qwen 3.6-35B

Contextless Signature Prompt Self-Healing

470 495 827

9 0 39

23 29 127

0 0 10

438 466 651

Qwen 3-Coder-30B

Contextless Signature Prompt Self-Healing

1,510 205 1,893

579 53 589

657 16 569

15 47 351

46 29 101

Contextless Signature Prompt Self-Healing

910 861 280

430 557 182

350 77 14

23 0 27

56 224 52

Contextless Signature Prompt Self-Healing

1,016 562 1,008

489 145 368

209 5 217

25 41 110

251 369 296

Qwen 3.5-9B

Gemma 4-31B

A. Summary of Findings Our evaluation of seven open-weight models across three prompting tiers shows critical insights into the automated synthesis of formally verified software. RQ1 [Contextless Prompting]: Our experiments show that while most LLMs fail to generate verifiable Dafny code from raw requirements, Gemma 4-31B and Codestral-22B demonstrate a surprising aptitude for the task. Specifically, Gemma 4-31B achieved a peak verify@5 success rate of 54.55% at T = 0.2. However, the 0% success rate of the remaining five models suggests that without structural guidance or external context, most systems struggle to navigate the strict formal constraints of the Dafny language. • RQ2 [Signature Prompting]: Providing the method signature as additional context drastically improved performance across the board, reversing the widespread failures observed in RQ1. Most notably, GPT-OSS-120B rose from a 0% success rate to 63.64%, while the smaller Qwen 3.5-9B achieved the highest overall verify@5 score of 72.73% at T = 0.8. These results indicate that the primary bottleneck in verifiable synthesis is the structural mapping of requirements to formal signatures, rather than the generation of the underlying verification logic. • RQ3 [Self-Healing]: Iterative self-healing significantly amplifies success rates, provided a structural foundation (method signature) is present. Gemma 4-31B emerged as the most resilient model, achieving a near-perfect 90.91% success rate in contextless healing. Meanwhile, GPTOSS-120B achieved its performance ceiling (81.82%) only when signature-guided, suggesting that large-scale general purpose models require structural constraints to •

effectively interpret and act upon formal compiler feedback. • RQ4 [Error Distributions]: Our analysis of compilation failures shows that Syntax Errors are the primary barrier in contextless settings, often exceeding 80% of total failures for models like GPT-OSS-20B. While Signature Prompting significantly reduces syntax issues, it shifts the bottleneck to Verification Errors, particularly for the largest models. Notably, Self-Healing effectively converts semantic and syntax errors into verified solutions for most models, though Codestral-22B and Qwen 3-Coder-30B show a tendency to regress into higher syntax error counts during iterative repair, suggesting a struggle to maintain syntactic integrity under compiler-driven feedback. B. Discussion The results of this study suggest a shift in the paradigm of automated formal programming. While the scaling law often assumes that larger parameters equate to better reasoning, our findings indicate a more nuanced reality. The significant success of Gemma 4-31B, which achieved a near-perfect 90.91% success rate in self-healing, suggests that specific pretraining data density regarding formal and algorithmic logic is more critical than raw model size for the Dafny language. Furthermore, the transition from total failure in RQ1 (0% for most models) to high success in RQ3b underscores the necessity of a Verification-in-the-Loop approach. By utilizing the Dafny verifier and the Z3 SMT solver as a groundtruth reward signal, we effectively mitigate the common LLM issue of logical hallucinations. The integration of uDebug was essential to this framework; it ensured that models did not achieve verification through vacuous or trivial specifications

13

such as empty post-conditions but rather through functional correctness that holds up against rigorous edge cases. Finally, the structural bottleneck identified in RQ2 suggests that the future of automated formal methods lies in hybrid prompting strategies. Even the most capable models, like GPT-OSS-120B, require a structural skeleton (the method signature) to bridge the gap between natural language intent and mathematical proof. This suggests that LLMs should be viewed not as autonomous agents, but as sophisticated coprocessors that thrive when provided with high-level formal constraints to guide their stochastic exploration. VIII. T HREATS TO VALIDITY Following Siegmund et al. [68] and Feldt and Magazinius [23], we identified several threats to the validity of this study. The deterministic nature of our verification criteria, relying on the Dafny verifier’s acceptance and the success of the uDebug test suite, is designed to ensure construct and internal validity. By using the formal verifier and the Z3 SMT solver as a ground-truth oracle, we eliminate human subjectivity in assessing whether the AI assisted synthesized code meets the formal requirements. External validity concerns the generalizability of our results to other models and languages. We acknowledge that the open-weight landscape, featuring models like Gemma 4-31B, Qwen 3.6-35B, and GPT-OSS-120B, is evolving rapidly. Our findings are specific to the contemporary architectures and the Dafny 4.11.0 verification engine. While we expect the success rates to improve with future iterations, the performance disparities observed particularly the structural bottleneck in contextless prompting. The issue likely represents a fundamental challenge in mapping natural language to formal logic that persists across model generations. A specific threat to external validity is vacuous verification, where a model satisfies the verifier with trivial specifications (e.g., ensures true). We mitigated this threat through our dual-layer validation pipeline. By requiring all verified methods to pass the uDebug functional test suites, we ensure that our results represent genuine functional correctness rather than mere logical consistency with a weak or empty specification. This approach strengthens the claim that the models are reasoning rather than satisfying the solver’s constraints. While our dataset introduces the first verified Dafny implementations for these UVa problems, there remains a risk that models may leverage cross-lingual knowledge of the underlying algorithms from more prevalent languages like C++ or Python. However, we mitigate this by focusing our evaluation on the synthesis of formal specifications and loop invariant constructs that are uniquely absent from standard competitive programming solutions. Finally, to ensure reproducibility despite the rapid development of these tools, we have documented the precise hardware configurations (NVIDIA RTX 6000 Ada) and software versions (LM Studio 0.4.8, Python 3.14.4) used. The research artifacts, including the NL2VC-60 dataset and our synthesis pipeline, are provided to allow for verification of these results.

IX. C ONCLUSION We investigated the potential of contemporary open-weight LLMs to synthesize formally verified methods and specifications in the Dafny programming language. Utilizing the NL2VC-60 dataset, we evaluated tiered prompting strategies across seven state-of-the-art models. Our findings confirm that while contextless natural language prompts generally lead to synthesis failure due to a structural bottleneck, tiered strategies incorporating formal method signatures and iterative selfhealing allow models to overcome the scarcity of specialized training data. Notably, Gemma 4-31B emerged as a highly resilient verification assistant, achieving a peak success rate of 90.91%, while the GPT-OSS-120B demonstrated the most significant performance leap when transitioned to a signatureguided healing pipeline. Our results demonstrate that an iterative feedback loop utilizing direct SMT-solver output, combined with structural anchors, yielded the highest performance ceiling. The orchestrated self-healing pipeline achieved a verification success rate of 81.82% for the 120B model and nearly 91% for the 31B model. By integrating the uDebug platform, we confirmed that these verified solutions are not only logically consistent but also functionally robust against extreme edge cases, effectively mitigating the risk of vacuous verification. These findings underscore the importance of Verification-inthe-Loop architectures and suggest that open-weight models can significantly lower the specification challenges. Our study suggests that the high success rates achieved by these models represent a several-thousand-fold cost reduction compared to human expert synthesis, making high-assurance software economically viable for general engineering tasks. Ultimately, the integration of formal oracles and generative models represents a vital path toward a future of trustworthy, AI-assisted software engineering where code is not plausible, but provably correct. R EFERENCES [1] [n. d.]. Microsoft Copilot: Your AI Companion. https: //copilot.microsoft.com/ Accessed: 2026-04-21. [2] 2026. UVa Online Judge. https://onlinejudge.org/. Accessed: 2026-04-19. [3] Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. 2023. Gpt-4 technical report. arXiv preprint arXiv:2303.08774 (2023). [4] Alibaba Qwen Team. 2025. Qwen3-Coder-30B: Specialized Models for Agentic Code Intelligence. https: //huggingface.co/Qwen Accessed: Apr. 22, 2026. [5] Alibaba Qwen Team. 2026. Qwen3.5 and Qwen3.6-MoE: Advancing Open-Weight Foundation Models. https:// github.com/QwenLM/Qwen Accessed: Apr. 22, 2026. [6] Amazon Web Services, Inc. 2024. Amazon Q Developer: AI coding companion. https://aws.amazon.com/q/ developer/ Accessed: 2026-04-21. [7] Anysphere, Inc. 2024. Cursor: The AI Code Editor. https://cursor.com/ Accessed: 2026-04-21.

14

[8] Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, et al. 2021. Program synthesis with large language models. arXiv preprint arXiv:2108.07732 (2021). [9] Mantas Baksys, Stefan Zetzsche, Olivier Bouissou, Remi Delmas, Soonho Kong, and Sean B Holden. 2025. ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis. arXiv preprint arXiv:2512.10173 (2025). [10] Debangshu Banerjee, Olivier Bouissou, and Stefan Zetzsche. 2026. DafnyPro: LLM-Assisted Automated Verification for Dafny Programs. arXiv preprint arXiv:2601.05385 (2026). [11] Clark Barrett, Leonardo De Moura, and Aaron Stump. 2005. SMT-COMP: Satisfiability modulo theories competition. In International Conference on Computer Aided Verification. Springer, 20–23. [12] Ruisheng Cao, Mouxiang Chen, Jiawei Chen, Zeyu Cui, Yunlong Feng, Binyuan Hui, Yuheng Jing, Kaixin Li, Mingze Li, Junyang Lin, et al. 2026. Qwen3-codernext technical report. arXiv preprint arXiv:2603.00729 (2026). [13] Franck Cassez, Joanne Fuller, Milad K Ghale, David J Pearce, and Horacio MA Quiles. 2023. Formal and executable semantics of the ethereum virtual machine in dafny. In International Symposium on Formal Methods. Springer, 571–583. [14] Aleksandar Chakarov, Aleksandr Fedchin, Zvonimir Rakamarić, and Neha Rungta. 2022. Better counterexamples for Dafny. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 404–411. [15] Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde De Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. 2021. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374 (2021). [16] Byron Cook. 2018. Formal reasoning about the security of amazon web services. In International Conference on Computer Aided Verification. Springer, 38–47. [17] Jade Copet, Quentin Carbonneaux, Gal Cohen, Jonas Gehring, Jacob Kahn, Jannik Kossen, Felix Kreuk, Emily McMilin, Michel Meyer, Yuxiang Wei, et al. 2025. Cwm: An open-weights llm for research on code generation with world models. arXiv preprint arXiv:2510.02387 (2025). [18] Łukasz Czajka, Burak Ekici, and Cezary Kaliszyk. 2018. Concrete semantics with Coq and CoqHammer. In International Conference on Intelligent Computer Mathematics. Springer, 53–59. [19] Dafny Team. 2024. Dafny Reference Manual. Dafny Software Foundation. https://dafny.org/ Accessed: 202604-20. [20] Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340. [21] Nusrat Farzana Dipu, Muhammad Monir Hossain,

Kimia Zamiri Azar, Farimah Farahmandi, and Mark Tehranipoor. 2024. Formalfuzzer: Formal verification assisted fuzz testing for soc vulnerability detection. In 2024 29th Asia and South Pacific Design Automation Conference (ASP-DAC). IEEE, 355–361. [22] Aleksandr Fedchin, Tyler Dean, Jeffrey S. Foster, et al. 2023. A Toolkit for Automated Testing of Dafny. Amazon Science (2023). https://www.amazon.science/ publications/a-toolkit-for-automated-testing-of-dafny [23] Robert Feldt and Ana Magazinius. 2010. Validity threats in empirical software engineering research-an initial survey.. In Seke. 374–379. [24] Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. 2023. Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 1229–1241. [25] Simon Frieder, Luca Pinchetti, Chevalier Chevalier, Ryan-Rhys Griffiths, Tommaso Salvatori, Thomas Lukasiewicz, Philipp Petersen, and Julius Berner. 2023. Mathematical capabilities of chatgpt. Advances in neural information processing systems 36 (2023), 27699– 27744. [26] Hubert Garavel, Maurice H Ter Beek, and Jaco Van De Pol. 2020. The 2020 expert survey on formal methods. In International Conference on Formal Methods for Industrial Critical Systems. Springer, 3–69. [27] Louie Giray. 2023. Prompt engineering with ChatGPT: a guide for academic writers. Annals of biomedical engineering 51, 12 (2023), 2629–2633. [28] GitHub Community. 2026. Dafny Repositories Search Results. https://github.com/search?q=dafny&type= repositories Accessed: 2026-04-23. [29] Google. 2024. Vibe Coding in Google AI Studio: Building Apps with Natural Language. https://aistudio.google. com/vibe-code Accessed: Apr. 22, 2026. [30] Google DeepMind. 2026. Gemma 4: Next-Generation Open Multimodal Models. https://ai.google.dev/gemma Accessed: Apr. 22, 2026. [31] Aaron Grattafiori, Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Alex Vaughan, et al. 2024. The llama 3 herd of models. arXiv preprint arXiv:2407.21783 (2024). [32] Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. 2017. Program synthesis. Foundations and Trends in Programming Languages 4, 1-2 (2017), 1–119. [33] Charles Antony Richard Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (1969), 576–580. [34] Ahmed Irfan, Sorawee Porncharoenwase, Zvonimir Rakamarić, Neha Rungta, and Emina Torlak. 2022. Testing Dafny (experience paper). In Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis. 556–567. [35] Ziwei Ji, Nayeon Lee, Rita Frieske, Tiezheng Yu, Dan Su, Yan Xu, Etsuko Ishii, Ye Jin Bang, Andrea Madotto,

15

and Pascale Fung. 2023. Survey of hallucination in natural language generation. ACM computing surveys 55, 12 (2023), 1–38. [36] Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. 2022. Thor: Wielding hammers to integrate language models and automated theorem provers. Advances in Neural Information Processing Systems 35 (2022), 8360–8373. [37] Cliff B Jones and Jayadev Misra. 2021. Theories of programming: the life and works of Tony Hoare. ACM. [38] Aishwarya Kamath, Johan Ferret, Shreya Pathak, Nino Vieillard, Ramona Merhej, Sarah Perrin, Tatiana Matejovicova, Alexandre Ramé, Morgane Rivière, Louis Rouillard, et al. 2025. Gemma 3 technical report. arXiv preprint arXiv:2503.19786 4 (2025). [39] Gerwin Klein, Philip Derrin, and Kevin Elphinstone. 2009. Experience report: sel4: formally verifying a highperformance microkernel. In Proceedings of the 14th ACM SIGPLAN international conference on Functional programming. 91–96. [40] Sumith Kulal, Panupong Pasupat, Kartik Chandra, Mina Lee, Oded Padon, Alex Aiken, and Percy S Liang. 2019. Spoc: Search-based pseudocode to code. Advances in Neural Information Processing Systems 32 (2019). [41] Claire Le Goues, K Rustan M Leino, and Michał Moskal. 2011. The boogie verification debugger (tool paper). In International Conference on Software Engineering and Formal Methods. Springer, 407–414. [42] K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In International conference on logic for programming artificial intelligence and reasoning. Springer, 348–370. [43] K Rustan M Leino. 2012. Developing verified programs with Dafny. In Proceedings of the 2012 ACM conference on High integrity language technology. 9–10. [44] Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (2009), 107–115. [45] Xavier Leroy. 2025. The CompCert C verified compiler: Documentation and user’s manual. Ph. D. Dissertation. Inria. [46] Grace A Lewis, Santiago Comella-Dorda, David P Gluch, John Hudak, and Charles Weinstock. 2001. Model-based verification: Analysis guidelines. Technical Report. [47] Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu. 2022. Qafny: A quantum-program verifier. arXiv preprint arXiv:2211.06411 (2022). [48] Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, and Max Tegmark. 2024. Dafnybench: A benchmark for formal software verification. arXiv preprint arXiv:2406.08467 (2024). [49] 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). IEEE, 16–28.

[50] Aman Madaan, Shuyan Zhou, Uri Alon, Yiming Yang, and Graham Neubig. 2022. Language models of code are few-shot commonsense learners. In Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing. 1384–1403. [51] Md Motaleb Hossen Manik and Ge Wang. 2026. Gemma 4, Phi-4, and Qwen3: Accuracy-Efficiency Tradeoffs in Dense and MoE Reasoning Language Models. arXiv preprint arXiv:2604.07035 (2026). [52] Ali Mesbah, Arie Van Deursen, and Danny Roest. 2011. Invariant-based automatic testing of modern web applications. IEEE Transactions on Software Engineering 38, 1 (2011), 35–53. [53] Microsoft Research. 2024. Dafny: A Language and Program Verifier for Functional Correctness. https://www.microsoft.com/en-us/research/project/ dafny-a-language-and-program-verifier-for-functional-correctness/ Official Project Page. [54] Mistral AI. 2024. Codestral-22B-v0.1: An Open-Weight Model for Professional Coders. https://mistral.ai/news/ codestral/ Accessed: Apr. 22, 2026. [55] Md Rakib Hossain Misu, Cristina V Lopes, Iris Ma, and James Noble. 2024. Towards ai-assisted synthesis of verified dafny methods. Proceedings of the ACM on Software Engineering 1, FSE (2024), 812–835. [56] Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. 2013. seL4: from general purpose to a proof of information flow enforcement. In 2013 IEEE Symposium on Security and Privacy. IEEE, 415–429. [57] Anthony Narkawicz, César A Munoz, and Aaron M Dutle. 2017. The MINERVA software development process. In NASA Formal Methods Symposium (NFM) 2017. [58] Noor Nashid, Mifta Sintaha, and Ali Mesbah. 2023. Retrieval-based prompt selection for code-related fewshot learning. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). IEEE, 2450–2462. [59] James Noble, David Streader, Isaac Oscar Gariano, and Miniruwani Samarakoon. 2022. More programming than programming: Teaching formal methods in a software engineering programme. In NASA Formal Methods Symposium. Springer, 431–450. [60] OpenAI. 2025. Introducing GPT-OSS: OpenWeight Reasoning Models. https://openai.com/ index/introducing-gpt-oss/ Accessed: Apr. 22, 2026. [61] Saswata Paul, Elkin Cruz, Airin Dutta, Ankita Bhaumik, Erik Blasch, Gul Agha, Stacy Patterson, Fotis Kopsaftopoulos, and Carlos Varela. 2023. Formal verification of safety-critical aerospace systems. IEEE Aerospace and Electronic Systems Magazine 38, 5 (2023), 72–88. [62] Partha Pratim Ray. 2025. A review on vibe coding: Fundamentals, state-of-the-art, challenges and future directions. Authorea Preprints (2025). [63] Laria Reynolds and Kyle McDonell. 2021. Prompt programming for large language models: Beyond the

16

few-shot paradigm. In Extended abstracts of the 2021 CHI conference on human factors in computing systems. 1–7. [64] Talia Ringer, Karl Palmskog, Ilya Sergey, Gligoric Milos, and Zachary Tatlock. 2019. QED at large: A survey of engineering of formally verified software. Foundations and Trends in Programming Languages 5, 2-3 (2019), 102–281. [65] JM Rushby. 1995. Model checking and other ways of automating formal methods. Position paper for panel on model checking for concurrent programs, Software Quality Week, San Francisco (1995). [66] Ahmed Ryan, Ibrahim Khalil, Abdullah Al Jahid, Md Erfan, Sungbin Park, Akond Ashfaque Ur Rahman, and Md Rayhanur Rahman. 2026. Mind the Gap: Evaluating LLMs for High-Level Malicious Package Detection vs. Fine-Grained Indicator Identification. arXiv preprint arXiv:2602.16304 (2026). [67] Andrew Sellergren, Sahar Kazemzadeh, Tiam Jaroensri, Atilla Kiraly, Madeleine Traverse, Timo Kohlberger, Shawn Xu, Fayaz Jamil, Cían Hughes, Charles Lau, et al. 2025. Medgemma technical report. arXiv preprint arXiv:2507.05201 (2025). [68] Janet Siegmund, Norbert Siegmund, and Sven Apel. 2015. Views on internal and external validity in empirical software engineering. In 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, Vol. 1. IEEE, 9–19. [69] Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. 2024. Clover: Clo sed-loop ver ifiable code generation. In International Symposium on AI Verification. Springer, 134–155. [70] Maurice ter Beek, Manfred Broy, and Brijesh Dongol. 2024. The role of formal methods in computer science education. ACM Inroads 15, 4 (2024), 58–66. [71] The Dafny Project. 2024. Dafny NuGet Package: The Dafny Compiler and Verifier. NuGet Package Manager. https://www.nuget.org/packages/Dafny/ Version 4.x.x, Accessed: Apr. 22, 2026. [72] The Dafny Project. 2024. Dafny Reference Manual. Amazon Web Services. https://dafny.org/latest/ DafnyRef/DafnyRef Accessed: Apr. 22, 2026. [73] Norbert Tihanyi, Yiannis Charalambous, Ridhi Jain, Mohamed Amine Ferrag, and Lucas C Cordeiro. 2025. A new era in software security: Towards self-healing software via large language models and formal verification. In 2025 IEEE/ACM International Conference on Automation of Software Test (AST). IEEE, 136–147. [74] Sergey Troshin, Wafaa Mohammed, Yan Meng, Christof Monz, Antske Fokkens, and Vlad Niculae. 2025. Control the Temperature: Selective Sampling for Diverse and High-Quality LLM Outputs. arXiv preprint arXiv:2510.01218 (2025). [75] Rosalia Tufano, Luca Pascarella, and Gabriele Bavota. 2023. Automating code-related tasks through transformers: The impact of pre-training. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). IEEE, 2425–2437.

[76] uDebug Team. 2026. uDebug: Online Debugging Tool for Competitive Programming. https://www.udebug. com/. Accessed: 2026-04-19. [77] UVa Online Judge. 2010. Problem 11934: Magic Formula. https://onlinejudge.org/external/119/11934.pdf. Accessed: 2026-04-21. [78] UVa Online Judge. n.d.. UVa Online Judge. https:// onlinejudge.org/. Accessed: 2026-04-20. [79] Changjie Wang, Mariano Scazzariello, Dejan Kostić, and Marco Chiesa. [n. d.]. Toward Automated, Contamination-free Dafny Benchmark Generation. ([n. d.]). [80] Yue Wang, Hung Le, Akhilesh Gotmare, Nghi Bui, Junnan Li, and Steven Hoi. 2023. Codet5+: Open code large language models for code understanding and generation. In Proceedings of the 2023 conference on empirical methods in natural language processing. 1069–1088. [81] Jules White, Quchen Fu, Sam Hays, Michael Sandborn, Carlos Olea, Henry Gilbert, Ashraf Elnashar, Jesse Spencer-Smith, and Douglas C Schmidt. 2023. A prompt pattern catalog to enhance prompt engineering with chatgpt. arXiv preprint arXiv:2302.11382 (2023). [82] Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with large language models. Advances in neural information processing systems 35 (2022), 32353–32368. [83] An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, et al. 2025. Qwen3 technical report. arXiv preprint arXiv:2505.09388 (2025). [84] Zhenkun Yang, Wen Wang, Jeremy Casas, Pasquale Cocchini, and Jin Yang. 2023. Towards a correct-byconstruction FHE model. Cryptology ePrint Archive (2023).