CINXE.COM

<!DOCTYPE html> <html lang="en"> <head> <meta content="text/html; charset=utf-8" http-equiv="content-type"/> <title>Can LLMs Enable Verification in Mainstream Programming?</title>  <meta content="width=device-width, initial-scale=1, shrink-to-fit=no" name="viewport"/> <link href="https://cdn.jsdelivr.net/npm/bootstrap@5.3.0/dist/css/bootstrap.min.css" rel="stylesheet" type="text/css"/> <link href="/static/browse/0.3.4/css/ar5iv.0.7.9.min.css" rel="stylesheet" type="text/css"/> <link href="/static/browse/0.3.4/css/ar5iv-fonts.0.7.9.min.css" rel="stylesheet" type="text/css"/> <link href="/static/browse/0.3.4/css/latexml_styles.css" rel="stylesheet" type="text/css"/> <script src="https://cdn.jsdelivr.net/npm/bootstrap@5.3.0/dist/js/bootstrap.bundle.min.js"></script> <script src="https://cdnjs.cloudflare.com/ajax/libs/html2canvas/1.3.3/html2canvas.min.js"></script> <script src="/static/browse/0.3.4/js/addons_new.js"></script> <script src="/static/browse/0.3.4/js/feedbackOverlay.js"></script> <base href="/html/2503.14183v1/"/></head> <body> <nav class="ltx_page_navbar"> <nav class="ltx_TOC"> <ol class="ltx_toclist"> <li class="ltx_tocentry ltx_tocentry_section"><a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S1" title="In Can LLMs Enable Verification in Mainstream Programming?">1 Introduction</a></li> <li class="ltx_tocentry ltx_tocentry_section"> <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S2" title="In Can LLMs Enable Verification in Mainstream Programming?">2 Method</a> <ol class="ltx_toclist ltx_toclist_section"> <li class="ltx_tocentry ltx_tocentry_subsection"><a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S2.SS1" title="In 2 Method ‣ Can LLMs Enable Verification in Mainstream Programming?">2.1 Task Preparation for Different Modes</a></li> <li class="ltx_tocentry ltx_tocentry_subsection"><a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S2.SS2" title="In 2 Method ‣ Can LLMs Enable Verification in Mainstream Programming?">2.2 Interaction with an LLM</a></li> <li class="ltx_tocentry ltx_tocentry_subsection"><a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S2.SS3" title="In 2 Method ‣ Can LLMs Enable Verification in Mainstream Programming?">2.3 Validation</a></li> <li class="ltx_tocentry ltx_tocentry_subsection"><a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S2.SS4" title="In 2 Method ‣ Can LLMs Enable Verification in Mainstream Programming?">2.4 Benchmarks</a></li> </ol> </li> <li class="ltx_tocentry ltx_tocentry_section"> <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S3" title="In Can LLMs Enable Verification in Mainstream Programming?">3 Evaluation</a> <ol class="ltx_toclist ltx_toclist_section"> <li class="ltx_tocentry ltx_tocentry_subsection"><a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S3.SS1" title="In 3 Evaluation ‣ Can LLMs Enable Verification in Mainstream Programming?">3.1 Understanding Common Pitfalls</a></li> </ol> </li> <li class="ltx_tocentry ltx_tocentry_section"><a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S4" title="In Can LLMs Enable Verification in Mainstream Programming?">4 Conclusion</a></li> </ol></nav> </nav> <div class="ltx_page_main"> <div class="ltx_page_content"> <article class="ltx_document ltx_authors_1line">11institutetext: JetBrains Research, Amsterdam, the Netherlands 22institutetext: Constructor University, Bremen, Germany 33institutetext: Neapolis University, Pafos, Cyprus <h1 class="ltx_title ltx_title_document">Can LLMs Enable Verification in Mainstream Programming?</h1> <div class="ltx_authors"> Aleksandr Shefer 1122 Igor Engel 1122 Stanislav Alekseev 1133 Daniil Berezun 11 Ekaterina Verbitskaia 1122 Anton Podkopaev 1122 </div> <div class="ltx_abstract"> <h6 class="ltx_title ltx_title_abstract">Abstract</h6> Although formal methods are capable of producing reliable software, they have seen minimal adoption in everyday programming. Automatic code generation using large language models is becoming increasingly widespread, but it rarely considers producing strong correctness guarantees. In this study, we explore the ability of LLMs to produce verified code in three verification languages (Dafny, Nagini, and Verus). To do so, we use manually curated datasets derived from the state-of-the-art Python benchmark, HumanEval. We also assess what types of information are sufficient to achieve good-quality results. </div> <section class="ltx_section" id="S1"> <h2 class="ltx_title ltx_title_section"> 1 Introduction</h2> <div class="ltx_para" id="S1.p1"> The cost of software failures only in the US is estimated to reach trillions of dollars a year <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib16" title="">16</a>]</cite>. Ever since the advent of large language models, a multitude of code generators have been developed. With people slowly beginning to trust these systems, significantly less time is spent critically evaluating the produced code. As a result, errors are more likely to find their way into codebases, leading to unintended consequences. Thus, it is of paramount importance to ensure the correctness of the generated code. </div> <div class="ltx_para" id="S1.p2"> Formal methods help programmers prevent avoidable mistakes by offering tools to analyse and prove the correctness of their code. It is most well-adopted in the areas where a mistake can have severe consequences, such as cryptography <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib33" title="">33</a>]</cite>, finance <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib4" title="">4</a>]</cite>, and aerospace <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib28" title="">28</a>]</cite>. Unfortunately, verification requires extensive expertise and extends the time necessary to create programs, which prevents its use in less safety-critical domains. </div> <div class="ltx_para" id="S1.p3"> Systems such as Dafny and F* automate proof search through the use of Satisfiability Modulo Theories (SMT) solvers, lowering the amount of effort needed for verification of complex properties. However, these verifiers feature specialized programming languages for both implementation and proofs. In order to introduce certified code into a software project, one has to commit to using a new language, which frequently entails less mature developer environments, limited interoperability with mainstream languages, and a steeper learning curve for the engineers. </div> <div class="ltx_para" id="S1.p4"> A promising solution to this problem comes in a form of intermediate verification languages such as Viper <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib23" title="">23</a>]</cite>. With this approach, an algorithm can be implemented in a restricted subset of a popular programming language directly and then supplemented with formal specification and proofs. This helps bridge the gap between mainstream programming and formal methods, reducing the barriers for adoption. The key challenge is then ensuring that reasoning about the program remains as straightforward as possible. </div> <div class="ltx_para" id="S1.p5"> A lot of effort has been put into solving this challenge over the years. There are many obstacles to the problem of automated software verification and synthesis. The most crucial stems from the undecidability of automatic loop invariant synthesis. There are many classical approaches to tackle the problem, including dynamic detection of likely invariants <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib18" title="">18</a>, <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib11" title="">11</a>, <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib3" title="">3</a>]</cite>, inductive invariant synthesis <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib26" title="">26</a>, <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib2" title="">2</a>, <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib8" title="">8</a>]</cite>, data-driven approaches <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib20" title="">20</a>, <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib19" title="">19</a>, <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib13" title="">13</a>]</cite>, deductive synthesis <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib32" title="">32</a>]</cite>, and non-linear reasoning <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib15" title="">15</a>, <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib29" title="">29</a>]</cite>. Most state-of-the-art tools, which provide any guarantees of soundness and correctness, rely on SMT-solvers to infer invariants for recursion and iteration. This is notably true for intermediate verification languages like Viper and Verus, as well as F* and Dafny. In this research, we do not focus on improving the underlined theory neither do we attempt to refine solvers’ results, leaving this important task to the designers and researches of SMT-solvers and verification languages. Instead, we aim to determine the extent to which modern LLMs are capable of bridging the existing gap and generate invariants for these languages that can be successfully verified by solvers. </div> <div class="ltx_para" id="S1.p6"> Generative AI solutions have been able to achieve rather high success rates in producing partial <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib22" title="">22</a>, <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib27" title="">27</a>, <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib14" title="">14</a>]</cite> and complete <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib31" title="">31</a>, <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib25" title="">25</a>, <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib7" title="">7</a>]</cite> proofs for existing code, as well as inferring postconditions based on textual descriptions <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib10" title="">10</a>]</cite> and complete verified code in Dafny <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib30" title="">30</a>]</cite>, Rust <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib1" title="">1</a>]</cite>, and F* <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib5" title="">5</a>]</cite>. The ability of large language models to make progress towards automating formal verification for specialized systems suggests it may be possible to integrate formal methods into mainstream programming. </div> <div class="ltx_para" id="S1.p7"> In this paper, we explore the capability of LLMs in generating formally verified code across three different systems. Our focus lies on Nagini <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib9" title="">9</a>]</cite> and Verus <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib17" title="">17</a>]</cite> — the verifiers of subsets of popular programming languages Python and Rust. We also include Dafny into consideration, which serves as a baseline. In addition to this, we investigate what kind of problem specification is enough for the model to produce verified code by exposing different amounts of information to it. Finally, we prepare three datasets based on HumanEval <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib6" title="">6</a>]</cite> of high-quality, manually implemented, verified programs to function as reference solutions. </div> </section> <section class="ltx_section" id="S2"> <h2 class="ltx_title ltx_title_section"> 2 Method</h2> <div class="ltx_para" id="S2.p1"> Our overarching goal of simplifying the lives of programmers who may not be used to formal verification poses the following question: how much information do we have to expose to an LLM in order to successfully produce correct-by-construction code? Can AI only help with the inferring simple loop invariants and assertions to finish the proof based on the existing codebase? Would it be possible to also generate implementations and high-level specifications from a natural language description? As we have found out, the answer lies somewhere in between. In pursuit of this research goal, we designed a universal framework that prepares prompts and validates programs generated in several scenarios. In this section, we discuss the framework, the benchmarks, and the experiments conducted. </div> <figure class="ltx_figure" id="S2.F1"><svg class="ltx_picture ltx_centering" height="411.17" id="S2.F1.pic1" overflow="visible" version="1.1" width="343.51"><g fill="#000000" stroke="#000000" transform="translate(0,411.17) matrix(1 0 0 -1 0 0) translate(144.94,0) translate(0,408.24)"><g stroke-width="0.4pt"><path d="M 2.94 0 C 2.94 1.62 1.62 2.94 0 2.94 C -1.62 2.94 -2.94 1.62 -2.94 0 C -2.94 -1.62 -1.62 -2.94 0 -2.94 C 1.62 -2.94 2.94 -1.62 2.94 0 Z M 0 0" style="stroke:none"></path><g stroke="#000000"><path d="M -59.06 -98.43 h 118.11 v 39.37 h -118.11 Z" style="fill:none"></path></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 -41.53 -82.12)"><foreignobject height="12.15" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="83.06">Preprocessing</foreignobject></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 7.51 -42.83)"><foreignobject height="12.3" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="158.59">Reference Implementation</foreignobject></g><g stroke="#000000"><path d="M -82.66 -177.17 h 165.31 v 39.37 h -165.31 Z" style="fill:none"></path></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 -78.04 -162.28)"><foreignobject height="9.61" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="156.47">Interaction with the LLM</foreignobject></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 6.99 -121.57)"><foreignobject height="12.3" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="112">Prepared Program</foreignobject></g><g stroke="#000000"><path d="M -59.06 -255.91 h 118.11 v 39.37 h -118.11 Z" style="fill:none"></path></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 -34.8 -241.02)"><foreignobject height="9.61" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="69.61">Verification</foreignobject></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 8.24 -201.65)"><foreignobject height="9.61" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="62.27">Candidate</foreignobject></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 121 -201.58)"><foreignobject height="9.46" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="72.95">Minor Fixes</foreignobject></g><g stroke="#000000"><path d="M -59.06 -334.65 h 118.11 v 39.37 h -118.11 Z" style="fill:none"></path></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 -31.13 -319.77)"><foreignobject height="9.61" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="62.27">Validation</foreignobject></g><g stroke="#00E000" stroke-width="0.8pt"><path d="M 13.98 -393.7 C 13.98 -385.98 7.72 -379.72 0 -379.72 C -7.72 -379.72 -13.98 -385.98 -13.98 -393.7 C -13.98 -401.42 -7.72 -407.68 0 -407.68 C 7.72 -407.68 13.98 -401.42 13.98 -393.7 Z M 0 -393.7" style="fill:none"></path></g><g fill="#000000" stroke="#000000" stroke-width="0.8pt" transform="matrix(1.0 0.0 0.0 1.0 -5.77 -398.49)"><foreignobject height="9.58" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="11.53">✓</foreignobject></g><g stroke-width="0.8pt"><path d="M 0 -3.21 L 0 -55.18" style="fill:none"></path><g transform="matrix(0.0 -1.0 1.0 0.0 0 -55.18)"><path d="M 3.6 0 L -2.16 2.88 L 0 0 L -2.16 -2.88" style="stroke:none"></path></g></g><g stroke-width="0.8pt"><path d="M 0 -98.7 L 0 -133.92" style="fill:none"></path><g transform="matrix(0.0 -1.0 1.0 0.0 0 -133.92)"><path d="M 3.6 0 L -2.16 2.88 L 0 0 L -2.16 -2.88" style="stroke:none"></path></g></g><g stroke-width="0.8pt"><path d="M 0 -177.44 L 0 -212.66" style="fill:none"></path><g transform="matrix(0.0 -1.0 1.0 0.0 0 -212.66)"><path d="M 3.6 0 L -2.16 2.88 L 0 0 L -2.16 -2.88" style="stroke:none"></path></g></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 -91.33 -240.95)"><foreignobject height="9.46" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="17.3">No</foreignobject></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 68.69 -252.76)"><foreignobject height="9.46" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="75.22">Minor issues</foreignobject></g><g stroke-width="0.8pt"><path d="M -59.33 -236.22 C -90.06 -245.43 -113.66 -166.69 -86.38 -158.51" style="fill:none"></path><g transform="matrix(0.95789 0.28712 -0.28712 0.95789 -86.38 -158.51)"><path d="M 3.6 0 L -2.16 2.88 L 0 0 L -2.16 -2.88" style="stroke:none"></path></g></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 9.27 -280.32)"><foreignobject height="9.46" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="20.83">Yes</foreignobject></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 9.27 -359.06)"><foreignobject height="9.46" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="20.83">Yes</foreignobject></g><g stroke-width="0.8pt"><path d="M 0 -256.18 L 0 -291.4" style="fill:none"></path><g transform="matrix(0.0 -1.0 1.0 0.0 0 -291.4)"><path d="M 3.6 0 L -2.16 2.88 L 0 0 L -2.16 -2.88" style="stroke:none"></path></g></g><g stroke-dasharray="0.8pt,1.0pt" stroke-dashoffset="0.0pt" stroke-width="0.8pt"><path d="M 59.33 -236.22 C 99.48 -236.22 157.48 -246.62 157.48 -210.06" style="fill:none"></path><g transform="matrix(0.0 1.0 -1.0 0.0 157.48 -210.06)"><path d="M 3.6 0 L -2.16 2.88 L 0 0 L -2.16 -2.88" style="stroke:none"></path></g></g><g stroke-dasharray="0.8pt,1.0pt" stroke-dashoffset="0.0pt" stroke-width="0.8pt"><path d="M 157.48 -187.23 C 157.48 -155.84 114.33 -157.48 86.53 -157.48" style="fill:none"></path><g transform="matrix(-1.0 0.0 0.0 -1.0 86.53 -157.48)"><path d="M 3.6 0 L -2.16 2.88 L 0 0 L -2.16 -2.88" style="stroke:none"></path></g></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 -103.14 -319.69)"><foreignobject height="9.46" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="17.3">No</foreignobject></g></g><g stroke-width="0.8pt"><path d="M -59.33 -314.96 C -120.78 -324.17 -144.38 -166.69 -86.49 -158.01" style="fill:none"></path><g transform="matrix(0.98895 0.14821 -0.14821 0.98895 -86.49 -158.01)"><path d="M 3.6 0 L -2.16 2.88 L 0 0 L -2.16 -2.88" style="stroke:none"></path></g></g><g stroke-width="0.8pt"><path d="M 0 -334.92 L 0 -375.57" style="fill:none"></path><g transform="matrix(0.0 -1.0 1.0 0.0 0 -375.57)"><path d="M 3.6 0 L -2.16 2.88 L 0 0 L -2.16 -2.88" style="stroke:none"></path></g></g></g></svg> <figcaption class="ltx_caption ltx_centering">Figure 1: The overview of evaluating an LLM on a benchmark problem</figcaption> </figure> <div class="ltx_para" id="S2.p2"> The overall pipeline consists of four key parts, see Figure <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S2.F1" title="Figure 1 ‣ 2 Method ‣ Can LLMs Enable Verification in Mainstream Programming?">1</a>. First, task preparation involves populating prompts with the task description and specification formed from the reference implementation in the dataset. Next, interaction with the large language model takes place, where the input is fed into it to generate a candidate solution. Following this, we attempt verification of the code produced and if any issues are detected, the feedback is passed back to the LLM to refine its suggestion. An optional step may be conducted to post-process the generated code with the aim of fixing common minor issues. Finally, we validate whether the verified code meets the reference specification. The last step is important to ensure that the generated preconditions are not too weak and postconditions are not too strong. Now, let us describe the steps in more details. </div> <section class="ltx_subsection" id="S2.SS1"> <h3 class="ltx_title ltx_title_subsection"> 2.1 Task Preparation for Different Modes</h3> <div class="ltx_para" id="S2.SS1.p1"> The benchmarks we use for evaluation contain ground truth, namely complete verified code that solves tasks from the original HumanEval dataset along with their natural language descriptions. A solution to a problem may be as small as a single function accompanied by its formal specification, if it is enough for the verifier to establish correctness. However, the majority of the programs include multiple functions and methods, as well as additional lemmas, loop invariants, and assertions needed for verification. Depending on the program synthesis task, only certain parts of a program need to be exposed. To simplify experiments, we annotated these components and used the annotations in the preparation of the input data. </div> <div class="ltx_para" id="S2.SS1.p2"> Experiment modes describe various scenarios for which generation can be applied. In some of them, a model is expected to only finish the correctness proof of the existing code, while in the others it generates code from scratch. In different situations, we can assume either the presence of textual description of the problem or its absence. Naturally, the complexity of the task varies from one mode to another. To estimate the ability of LLMs to cope with different cases, we describe six modes, each of which requires appropriate preprocessing and a set of prompts. </div> <figure class="ltx_figure" id="S2.F2"> <div class="ltx_flex_figure"> <div class="ltx_flex_cell ltx_flex_size_1"> <figure class="ltx_figure ltx_figure_panel ltx_minipage ltx_align_top" id="S2.F2.sf1" style="width:195.1pt;"> <div class="ltx_listing ltx_lst_language_Dafny ltx_lstlisting ltx_listing" id="S2.F2.sf1.2"> <div class="ltx_listing_data"><a download="" href="data:text/plain;base64,ZnVuY3Rpb24gcHJvZChzOiBzZXE8aW50PikgOiBpbnQgewogIGlmIHxzfCA9PSAwIHRoZW4gMQogIGVsc2Ugc1swXSAqIHByb2Qoc1sxLi5dKQp9Cm1ldGhvZCBzdW1fcHJvZHVjdChudW1zOiBzZXE8aW50PikKICByZXR1cm5zIChzIDogaW50LCBwIDogaW50KQogIGVuc3VyZXMgcyA9PSBzdW0obnVtcykKICBlbnN1cmVzIHAgPT0gcHJvZChudW1zKQp7CiFcVmVydXNCRyEgIGFzc2VydCBudW1zWy4ufG51bXN8XSA9PSBudW1zOwogIHMgOj0gMCwgcCA6PSAxOwogIGZvciBpIDo9IDAgdG8gfG51bXN8CiFcVmVydXNCRyEgICAgaW52YXJpYW50IHMgPT0gc3VtKG51bXNbLi5pXSkKIVxWZXJ1c0JHISAgICBpbnZhcmlhbnQgcCA9PSBwcm9kKG51bXNbLi5pXSkKICAgIHsgcyA6PSBzICsgbnVtc1tpXTsKICAgICAgcCA6PSBwICogbnVtc1tpXTsgfSAuLi4gfQo=">⬇</a></div> <div class="ltx_listingline" id="lstnumberx1"> function prod(s: seq<int>) : int { </div> <div class="ltx_listingline" id="lstnumberx2"> if |s| == 0 then 1 </div> <div class="ltx_listingline" id="lstnumberx3"> else s[0] * prod(s[1..]) </div> <div class="ltx_listingline" id="lstnumberx4"> } </div> <div class="ltx_listingline" id="lstnumberx5"> method sum_product(nums: seq<int>) </div> <div class="ltx_listingline" id="lstnumberx6"> returns (s : int, p : int) </div> <div class="ltx_listingline" id="lstnumberx7"> ensures s == sum(nums) </div> <div class="ltx_listingline" id="lstnumberx8"> ensures p == prod(nums) </div> <div class="ltx_listingline" id="lstnumberx9"> { </div> <div class="ltx_listingline" id="lstnumberx10"> assert nums[..|nums|] == nums; </div> <div class="ltx_listingline" id="lstnumberx11"> s := 0, p := 1; </div> <div class="ltx_listingline" id="lstnumberx12"> for i := 0 to |nums| </div> <div class="ltx_listingline" id="lstnumberx13"> invariant s == sum(nums[..i]) </div> <div class="ltx_listingline" id="lstnumberx14"> invariant p == prod(nums[..i]) </div> <div class="ltx_listingline" id="lstnumberx15"> { s := s + nums[i]; </div> <div class="ltx_listingline" id="lstnumberx16"> p := p * nums[i]; } ... } </div> </div> <figcaption class="ltx_caption">(a) Mode 1</figcaption> </figure> </div> <div class="ltx_flex_break"></div> <div class="ltx_flex_cell ltx_flex_size_1"> <figure class="ltx_figure ltx_figure_panel ltx_minipage ltx_align_top" id="S2.F2.sf2" style="width:195.1pt;"> <div class="ltx_listing ltx_lst_language_Dafny ltx_lstlisting ltx_listing" id="S2.F2.sf2.2"> <div class="ltx_listing_data"><a download="" href="data:text/plain;base64,ZnVuY3Rpb24gcHJvZChzOiBzZXE8aW50PikgOiBpbnQgewogIGlmIHxzfCA9PSAwIHRoZW4gMQogIGVsc2Ugc1swXSAqIHByb2Qoc1sxLi5dKQp9Cm1ldGhvZCBzdW1fcHJvZHVjdChudW1zOiBzZXE8aW50PikKICByZXR1cm5zIChzIDogaW50LCBwIDogaW50KQohXFZlcnVzQkchICBlbnN1cmVzIHMgPT0gc3VtKG51bXMpCiFcVmVydXNCRyEgIGVuc3VyZXMgcCA9PSBwcm9kKG51bXMpCnsKIVxWZXJ1c0JHISAgYXNzZXJ0IG51bXNbLi58bnVtc3xdID09IG51bXM7CiAgcyA6PSAwLCBwIDo9IDE7CiAgZm9yIGkgOj0gMCB0byB8bnVtc3wKIVxWZXJ1c0JHISAgICBpbnZhcmlhbnQgcyA9PSBzdW0obnVtc1suLmldKQohXFZlcnVzQkchICAgIGludmFyaWFudCBwID09IHByb2QobnVtc1suLmldKQogICAgeyBzIDo9IHMgKyBudW1zW2ldOwogICAgICBwIDo9IHAgKiBudW1zW2ldOyB9IC4uLiB9">⬇</a></div> <div class="ltx_listingline" id="lstnumberx17"> function prod(s: seq<int>) : int { </div> <div class="ltx_listingline" id="lstnumberx18"> if |s| == 0 then 1 </div> <div class="ltx_listingline" id="lstnumberx19"> else s[0] * prod(s[1..]) </div> <div class="ltx_listingline" id="lstnumberx20"> } </div> <div class="ltx_listingline" id="lstnumberx21"> method sum_product(nums: seq<int>) </div> <div class="ltx_listingline" id="lstnumberx22"> returns (s : int, p : int) </div> <div class="ltx_listingline" id="lstnumberx23"> ensures s == sum(nums) </div> <div class="ltx_listingline" id="lstnumberx24"> ensures p == prod(nums) </div> <div class="ltx_listingline" id="lstnumberx25"> { </div> <div class="ltx_listingline" id="lstnumberx26"> assert nums[..|nums|] == nums; </div> <div class="ltx_listingline" id="lstnumberx27"> s := 0, p := 1; </div> <div class="ltx_listingline" id="lstnumberx28"> for i := 0 to |nums| </div> <div class="ltx_listingline" id="lstnumberx29"> invariant s == sum(nums[..i]) </div> <div class="ltx_listingline" id="lstnumberx30"> invariant p == prod(nums[..i]) </div> <div class="ltx_listingline" id="lstnumberx31"> { s := s + nums[i]; </div> <div class="ltx_listingline" id="lstnumberx32"> p := p * nums[i]; } ... } </div> </div> <figcaption class="ltx_caption">(b) Mode 2</figcaption> </figure> </div> <div class="ltx_flex_break"></div> <div class="ltx_flex_cell ltx_flex_size_1"> <figure class="ltx_figure ltx_figure_panel ltx_minipage ltx_align_top" id="S2.F2.sf3" style="width:195.1pt;"> <div class="ltx_listing ltx_lst_language_Dafny ltx_lstlisting ltx_listing" id="S2.F2.sf3.2"> <div class="ltx_listing_data"><a download="" href="data:text/plain;base64,ZnVuY3Rpb24gcHJvZChzOiBzZXE8aW50PikgOiBpbnQgewogIGlmIHxzfCA9PSAwIHRoZW4gMQogIGVsc2Ugc1swXSAqIHByb2Qoc1sxLi5dKQp9Cm1ldGhvZCBzdW1fcHJvZHVjdChudW1zOiBzZXE8aW50PikKICByZXR1cm5zIChzIDogaW50LCBwIDogaW50KQogIGVuc3VyZXMgcyA9PSBzdW0obnVtcykKICBlbnN1cmVzIHAgPT0gcHJvZChudW1zKQp7CiFcVmVydXNCRyEgIGFzc2VydCBudW1zWy4ufG51bXN8XSA9PSBudW1zOwohXFZlcnVzQkchICBzIDo9IDAsIHAgOj0gMTsKIVxWZXJ1c0JHISAgZm9yIGkgOj0gMCB0byB8bnVtc3wKIVxWZXJ1c0JHISAgICBpbnZhcmlhbnQgcyA9PSBzdW0obnVtc1suLmldKQohXFZlcnVzQkchICAgIGludmFyaWFudCBwID09IHByb2QobnVtc1suLmldKQohXFZlcnVzQkchICAgIHsgcyA6PSBzICsgbnVtc1tpXTsKIVxWZXJ1c0JHISAgICAgIHAgOj0gcCAqIG51bXNbaV07IH0gLi4uIH0=">⬇</a></div> <div class="ltx_listingline" id="lstnumberx33"> function prod(s: seq<int>) : int { </div> <div class="ltx_listingline" id="lstnumberx34"> if |s| == 0 then 1 </div> <div class="ltx_listingline" id="lstnumberx35"> else s[0] * prod(s[1..]) </div> <div class="ltx_listingline" id="lstnumberx36"> } </div> <div class="ltx_listingline" id="lstnumberx37"> method sum_product(nums: seq<int>) </div> <div class="ltx_listingline" id="lstnumberx38"> returns (s : int, p : int) </div> <div class="ltx_listingline" id="lstnumberx39"> ensures s == sum(nums) </div> <div class="ltx_listingline" id="lstnumberx40"> ensures p == prod(nums) </div> <div class="ltx_listingline" id="lstnumberx41"> { </div> <div class="ltx_listingline" id="lstnumberx42"> assert nums[..|nums|] == nums; </div> <div class="ltx_listingline" id="lstnumberx43"> s := 0, p := 1; </div> <div class="ltx_listingline" id="lstnumberx44"> for i := 0 to |nums| </div> <div class="ltx_listingline" id="lstnumberx45"> invariant s == sum(nums[..i]) </div> <div class="ltx_listingline" id="lstnumberx46"> invariant p == prod(nums[..i]) </div> <div class="ltx_listingline" id="lstnumberx47"> { s := s + nums[i]; </div> <div class="ltx_listingline" id="lstnumberx48"> p := p * nums[i]; } ... } </div> </div> <figcaption class="ltx_caption">(c) Mode 3</figcaption> </figure> </div> <div class="ltx_flex_break"></div> <div class="ltx_flex_cell ltx_flex_size_1"> <figure class="ltx_figure ltx_figure_panel ltx_minipage ltx_align_top" id="S2.F2.sf4" style="width:195.1pt;"> <div class="ltx_listing ltx_lst_language_Dafny ltx_lstlisting ltx_listing" id="S2.F2.sf4.2"> <div class="ltx_listing_data"><a download="" href="data:text/plain;base64,ZnVuY3Rpb24gcHJvZChzOiBzZXE8aW50PikgOiBpbnQgewogIGlmIHxzfCA9PSAwIHRoZW4gMQogIGVsc2Ugc1swXSAqIHByb2Qoc1sxLi5dKQp9Cm1ldGhvZCBzdW1fcHJvZHVjdChudW1zOiBzZXE8aW50PikKICByZXR1cm5zIChzIDogaW50LCBwIDogaW50KQogIGVuc3VyZXMgcyA9PSBzdW0obnVtcykKICBlbnN1cmVzIHAgPT0gcHJvZChudW1zKQp7CiFcVmVydXNCRyEgIGFzc2VydCBudW1zWy4ufG51bXN8XSA9PSBudW1zOwohXFZlcnVzQkchICBzIDo9IDAsIHAgOj0gMTsKIVxWZXJ1c0JHISAgZm9yIGkgOj0gMCB0byB8bnVtc3wKIVxWZXJ1c0JHISAgICBpbnZhcmlhbnQgcyA9PSBzdW0obnVtc1suLmldKQohXFZlcnVzQkchICAgIGludmFyaWFudCBwID09IHByb2QobnVtc1suLmldKQohXFZlcnVzQkchICAgIHsgcyA6PSBzICsgbnVtc1tpXTsKIVxWZXJ1c0JHISAgICAgIHAgOj0gcCAqIG51bXNbaV07IH0gLi4uIH0=">⬇</a></div> <div class="ltx_listingline" id="lstnumberx49"> function prod(s: seq<int>) : int { </div> <div class="ltx_listingline" id="lstnumberx50"> if |s| == 0 then 1 </div> <div class="ltx_listingline" id="lstnumberx51"> else s[0] * prod(s[1..]) </div> <div class="ltx_listingline" id="lstnumberx52"> } </div> <div class="ltx_listingline" id="lstnumberx53"> method sum_product(nums: seq<int>) </div> <div class="ltx_listingline" id="lstnumberx54"> returns (s : int, p : int) </div> <div class="ltx_listingline" id="lstnumberx55"> ensures s == sum(nums) </div> <div class="ltx_listingline" id="lstnumberx56"> ensures p == prod(nums) </div> <div class="ltx_listingline" id="lstnumberx57"> { </div> <div class="ltx_listingline" id="lstnumberx58"> assert nums[..|nums|] == nums; </div> <div class="ltx_listingline" id="lstnumberx59"> s := 0, p := 1; </div> <div class="ltx_listingline" id="lstnumberx60"> for i := 0 to |nums| </div> <div class="ltx_listingline" id="lstnumberx61"> invariant s == sum(nums[..i]) </div> <div class="ltx_listingline" id="lstnumberx62"> invariant p == prod(nums[..i]) </div> <div class="ltx_listingline" id="lstnumberx63"> { s := s + nums[i]; </div> <div class="ltx_listingline" id="lstnumberx64"> p := p * nums[i]; } ... } </div> </div> <figcaption class="ltx_caption">(d) Mode 4</figcaption> </figure> </div> <div class="ltx_flex_break"></div> <div class="ltx_flex_cell ltx_flex_size_1"> <figure class="ltx_figure ltx_figure_panel ltx_minipage ltx_align_top" id="S2.F2.sf5" style="width:195.1pt;"> <div class="ltx_listing ltx_lst_language_Dafny ltx_lstlisting ltx_listing" id="S2.F2.sf5.2"> <div class="ltx_listing_data"><a download="" href="data:text/plain;base64,ZnVuY3Rpb24gcHJvZChzOiBzZXE8aW50PikgOiBpbnQgewogIGlmIHxzfCA9PSAwIHRoZW4gMQogIGVsc2Ugc1swXSAqIHByb2Qoc1sxLi5dKQp9Cm1ldGhvZCBzdW1fcHJvZHVjdChudW1zOiBzZXE8aW50PikKICByZXR1cm5zIChzIDogaW50LCBwIDogaW50KQohXFZlcnVzQkchICBlbnN1cmVzIHMgPT0gc3VtKG51bXMpCiFcVmVydXNCRyEgIGVuc3VyZXMgcCA9PSBwcm9kKG51bXMpCnsKIVxWZXJ1c0JHISAgYXNzZXJ0IG51bXNbLi58bnVtc3xdID09IG51bXM7CiFcVmVydXNCRyEgIHMgOj0gMDsKIVxWZXJ1c0JHISAgcCA6PSAxOwohXFZlcnVzQkchICBmb3IgaSA6PSAwIHRvIHxudW1zfAohXFZlcnVzQkchICAgIGludmFyaWFudCBzID09IHN1bShudW1zWy4uaV0pCiFcVmVydXNCRyEgICAgaW52YXJpYW50IHAgPT0gcHJvZChudW1zWy4uaV0pCiFcVmVydXNCRyEgICAgeyBzIDo9IHMgKyBudW1zW2ldOwohXFZlcnVzQkchICAgICAgcCA6PSBwICogbnVtc1tpXTsgfSAuLi4gfQ==">⬇</a></div> <div class="ltx_listingline" id="lstnumberx65"> function prod(s: seq<int>) : int { </div> <div class="ltx_listingline" id="lstnumberx66"> if |s| == 0 then 1 </div> <div class="ltx_listingline" id="lstnumberx67"> else s[0] * prod(s[1..]) </div> <div class="ltx_listingline" id="lstnumberx68"> } </div> <div class="ltx_listingline" id="lstnumberx69"> method sum_product(nums: seq<int>) </div> <div class="ltx_listingline" id="lstnumberx70"> returns (s : int, p : int) </div> <div class="ltx_listingline" id="lstnumberx71"> ensures s == sum(nums) </div> <div class="ltx_listingline" id="lstnumberx72"> ensures p == prod(nums) </div> <div class="ltx_listingline" id="lstnumberx73"> { </div> <div class="ltx_listingline" id="lstnumberx74"> assert nums[..|nums|] == nums; </div> <div class="ltx_listingline" id="lstnumberx75"> s := 0; </div> <div class="ltx_listingline" id="lstnumberx76"> p := 1; </div> <div class="ltx_listingline" id="lstnumberx77"> for i := 0 to |nums| </div> <div class="ltx_listingline" id="lstnumberx78"> invariant s == sum(nums[..i]) </div> <div class="ltx_listingline" id="lstnumberx79"> invariant p == prod(nums[..i]) </div> <div class="ltx_listingline" id="lstnumberx80"> { s := s + nums[i]; </div> <div class="ltx_listingline" id="lstnumberx81"> p := p * nums[i]; } ... } </div> </div> <figcaption class="ltx_caption">(e) Mode 5</figcaption> </figure> </div> <div class="ltx_flex_break"></div> <div class="ltx_flex_cell ltx_flex_size_1"> <figure class="ltx_figure ltx_figure_panel ltx_minipage ltx_align_top" id="S2.F2.sf6" style="width:195.1pt;"> <div class="ltx_listing ltx_lst_language_Dafny ltx_lstlisting ltx_listing" id="S2.F2.sf6.2"> <div class="ltx_listing_data"><a download="" href="data:text/plain;base64,IVxWZXJ1c0JHIWZ1bmN0aW9uIHByb2Qoczogc2VxPGludD4pIDogaW50IHsKIVxWZXJ1c0JHISAgaWYgfHN8ID09IDAgdGhlbiAxCiFcVmVydXNCRyEgIGVsc2Ugc1swXSAqIHByb2Qoc1sxLi5dKQohXFZlcnVzQkchfQptZXRob2Qgc3VtX3Byb2R1Y3QobnVtczogc2VxPGludD4pCiAgcmV0dXJucyAocyA6IGludCwgcCA6IGludCkKIVxWZXJ1c0JHISAgZW5zdXJlcyBzID09IHN1bShudW1zKQohXFZlcnVzQkchICBlbnN1cmVzIHAgPT0gcHJvZChudW1zKQp7CiFcVmVydXNCRyEgIGFzc2VydCBudW1zWy4ufG51bXN8XSA9PSBudW1zOwohXFZlcnVzQkchICBzIDo9IDA7CiFcVmVydXNCRyEgIHAgOj0gMTsKIVxWZXJ1c0JHISAgZm9yIGkgOj0gMCB0byB8bnVtc3wKIVxWZXJ1c0JHISAgICBpbnZhcmlhbnQgcyA9PSBzdW0obnVtc1suLmldKQohXFZlcnVzQkchICAgIGludmFyaWFudCBwID09IHByb2QobnVtc1suLmldKQohXFZlcnVzQkchICAgIHsgcyA6PSBzICsgbnVtc1tpXTsKIVxWZXJ1c0JHISAgICAgIHAgOj0gcCAqIG51bXNbaV07IH0gLi4uIH0=">⬇</a></div> <div class="ltx_listingline" id="lstnumberx82"> function prod(s: seq<int>) : int { </div> <div class="ltx_listingline" id="lstnumberx83"> if |s| == 0 then 1 </div> <div class="ltx_listingline" id="lstnumberx84"> else s[0] * prod(s[1..]) </div> <div class="ltx_listingline" id="lstnumberx85"> } </div> <div class="ltx_listingline" id="lstnumberx86"> method sum_product(nums: seq<int>) </div> <div class="ltx_listingline" id="lstnumberx87"> returns (s : int, p : int) </div> <div class="ltx_listingline" id="lstnumberx88"> ensures s == sum(nums) </div> <div class="ltx_listingline" id="lstnumberx89"> ensures p == prod(nums) </div> <div class="ltx_listingline" id="lstnumberx90"> { </div> <div class="ltx_listingline" id="lstnumberx91"> assert nums[..|nums|] == nums; </div> <div class="ltx_listingline" id="lstnumberx92"> s := 0; </div> <div class="ltx_listingline" id="lstnumberx93"> p := 1; </div> <div class="ltx_listingline" id="lstnumberx94"> for i := 0 to |nums| </div> <div class="ltx_listingline" id="lstnumberx95"> invariant s == sum(nums[..i]) </div> <div class="ltx_listingline" id="lstnumberx96"> invariant p == prod(nums[..i]) </div> <div class="ltx_listingline" id="lstnumberx97"> { s := s + nums[i]; </div> <div class="ltx_listingline" id="lstnumberx98"> p := p * nums[i]; } ... } </div> </div> <figcaption class="ltx_caption">(f) Mode 6</figcaption> </figure> </div> </div> <figcaption class="ltx_caption">Figure 2: The dark-yellow background highlights the parts of Dafny code required to be filled by an LLM in different modes.</figcaption> </figure> <div class="ltx_para" id="S2.SS1.p3"> Figure <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S2.F2" title="Figure 2 ‣ 2.1 Task Preparation for Different Modes ‣ 2 Method ‣ Can LLMs Enable Verification in Mainstream Programming?">2</a> illustrates the different artifacts used in prompts distilled from the ground truth in Dafny. The method in the figure computes the sum and the product of the numbers in the given sequence by iterating in a for-loop. The function prod is an example of a specification function which is not allowed to be used in the implementation. Notice that we have omitted some details, such as assertions, due to space constraints. In the figure, we highlight those lines that are not included into prompts. </div> <div class="ltx_para" id="S2.SS1.p4"> Mode 1 is the least demanding scenario and represents the basic case of generating only the proof by the given specification and code. While preprocessing, we erase all invariants, assertions and lemma calls from the target methods. What is left are pre- and postconditions, specification functions, method signatures and implementations, see Figure <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S2.F2.sf1" title="In Figure 2 ‣ 2.1 Task Preparation for Different Modes ‣ 2 Method ‣ Can LLMs Enable Verification in Mainstream Programming?">2(a)</a>. </div> <div class="ltx_para" id="S2.SS1.p5"> Mode 2 tests generation of both a specification and a proof solely from code. Thus, models are given complete implementations along with specification functions, but not verification primitives. </div> <div class="ltx_para" id="S2.SS1.p6"> Mode 3 targets a situation when a developer knows exactly how a method is supposed to work and can provide the exact specification of its behavior. The task of an AI-assistant is to fill in the implementation and the necessary hints enabling the verifier to finish the proof. </div> <div class="ltx_para" id="S2.SS1.p7"> Mode 4 differs from Mode 3 only by requiring a text description of the program. We believe this mode to be the most realistic and helpful use case of a tool like ours. </div> <div class="ltx_para" id="S2.SS1.p8"> The last two modes assess the capabilities of LLMs to generate everything from the implementation to a proof given only natural language specifications and method signatures. In Mode 5, we provide the additional context by including specification functions in the prompt. However, it can be easier to guess the user intent with these functions, so we omit them in Mode 6. </div> </section> <section class="ltx_subsection" id="S2.SS2"> <h3 class="ltx_title ltx_title_subsection"> 2.2 Interaction with an LLM</h3> <div class="ltx_para" id="S2.SS2.p1"> We start interacting with an LLM by sending a system and a user prompt. The former primes the LLM to act as an expert in a particular verification system (Dafny, Nagini, or Verus) and defines the expected output format. The user prompt details the task to be performed and offers guidance on code structure, examples in a chosen language, and optional tips on relevant constructs. Figure <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S2.F3" title="Figure 3 ‣ 2.2 Interaction with an LLM ‣ 2 Method ‣ Can LLMs Enable Verification in Mainstream Programming?">3</a> sketches the structure of the user prompt. </div> <figure class="ltx_figure" id="S2.F3"><svg class="ltx_picture ltx_centering" height="228.9" id="S2.F3.pic1" overflow="visible" version="1.1" width="295.83"><g fill="#000000" stroke="#000000" stroke-width="0.4pt" transform="translate(0,228.9) matrix(1 0 0 -1 0 0) translate(147.91,0) translate(0,208.94)"><g stroke="#000000"><path d="M -147.64 -19.69 h 295.28 v 39.37 h -295.28 Z" style="fill:none"></path></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 -127.95 -3.54)"><foreignobject height="12.3" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="255.91"> Mode description </foreignobject></g><g stroke="#000000"><path d="M -147.64 -66.93 h 295.28 v 39.37 h -295.28 Z" style="fill:none"></path></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 -127.95 -50.78)"><foreignobject height="12.3" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="255.91"> Optional: Language hints </foreignobject></g><g stroke="#000000"><path d="M -147.64 -114.17 h 295.28 v 39.37 h -295.28 Z" style="fill:none"></path></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 -127.95 -98.02)"><foreignobject height="12.3" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="255.91"> Optional: Verified code sample </foreignobject></g><g stroke="#000000"><path d="M -147.64 -161.42 h 295.28 v 39.37 h -295.28 Z" style="fill:none"></path></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 -127.95 -140.14)"><foreignobject height="22.56" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="255.91"> Optional: Textual description of the problem </foreignobject></g><g stroke="#000000"><path d="M -147.64 -208.66 h 295.28 v 39.37 h -295.28 Z" style="fill:none"></path></g><g fill="#000000" stroke="#000000" transform="matrix(1.0 0.0 0.0 1.0 -127.95 -192.51)"><foreignobject height="12.3" overflow="visible" transform="matrix(1 0 0 -1 0 16.6)" width="255.91"> Input code, prepared from ground truth </foreignobject></g></g></svg> <figcaption class="ltx_caption ltx_centering">Figure 3: The general structure of a prompt</figcaption> </figure> <div class="ltx_para" id="S2.SS2.p2"> After the LLM has produced a candidate solution, its verification is attempted. Whenever any issues are detected in the generated code, the feedback is collected and then used in a prompt to correct them. This request is repeated a few times until the failure has been successfully addressed, or a limit is reached. </div> <div class="ltx_para" id="S2.SS2.p3"> We have noticed that models tend to make minor mistakes when working on Nagini, mostly mixing up keywords and syntax structures. For example, double negations such as a < b < c are often produced even though they are not allowed in the system, likely because they are legal in Python. These kinds of errors can be fixed through non-ML means, which is both cheaper and faster than the counterpart. Thus, we implemented several simple syntactic converters to resolve such issues in Nagini and employ them prior to passing the incorrect candidate back to the LLM. </div> <div class="ltx_para" id="S2.SS2.p4"> It may seem to be sufficient to stop after verifiable code is produced. Unfortunately, it may not be the case, as models can misinterpret user intent, break the rules by erasing function definitions or simplifying pre- and postconditions. Because it was our intention not to admit such poor-quality responses, we employed additional validation state. For scenarios that do not require producing a specification, the validation helps to check that the original code has not been modified. For modes aimed at generating code along with a specification, it ensures it to be sufficiently complex and expressive. </div> </section> <section class="ltx_subsection" id="S2.SS3"> <h3 class="ltx_title ltx_title_subsection"> 2.3 Validation</h3> <div class="ltx_para" id="S2.SS3.p1"> When an LLM is tasked to determine formal properties that the code must satisfy, we need to ensure that generated pre- and postconditions correctly express user intentions. Prior research either manually checks the correctness and completeness of specifications <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib21" title="">21</a>]</cite> or exploits other LLMs to compare the specification and the natural language description <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib1" title="">1</a>]</cite>. Unfortunately, the former approach takes too much human effort, while the latter runs the risk of incorrectly assessing the quality due to the limitations of an LLM. Another strategy, introduced in the Clover framework <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib30" title="">30</a>]</cite>, involves a formal proof of equality between annotations. </div> <div class="ltx_para" id="S2.SS3.p2"> Inspired by Clover, we check specifications by utilizing SMT-solvers. However, instead of requiring equivalence, which may be too strict in practice, we check if the generated specification implies the specification as written in the reference solution in the data set. This way, we do not expect the LLM to guess the exact solution, giving it more freedom. In particular, the generated preconditions can be weaker and the postconditions can be stronger than the original. </div> <div class="ltx_para" id="S2.SS3.p3"> To achieve this goal, we perform validation after the LLM has generated code. Having a list of target methods from the initial template, we construct a wrapper for each of them, that has the same specification as the original method. In its body, the wrapper calls the original method and propagates the return value. For example, for the method sum_product from Figure <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S2.F2" title="Figure 2 ‣ 2.1 Task Preparation for Different Modes ‣ 2 Method ‣ Can LLMs Enable Verification in Mainstream Programming?">2</a>, we add a validator sum_product_valid that checks the pre- and postconditions. </div> <div class="ltx_para" id="S2.SS3.p4"> Despite this approach being automatic and reliable due to its deterministic nature, it has some drawbacks. Firstly, there are some limitations on which language features can be used. For example, functions must be used instead of predicates in Dafny, classes are disallowed, as well as open/closed in Verus. In addition to this, the validation comes with an additional verification overhead. Sometimes, when helpers are present, a verifier gives up trying to prove equality of the validation and the generated helpers, despite their indistinguishability. Finally, there might be multiple ways to specify the same user intent with sufficient accuracy. However, we always compare the code to the ground truth in our benchmarks, which might not scale well if more complicated tasks are considered. </div> </section> <section class="ltx_subsection" id="S2.SS4"> <h3 class="ltx_title ltx_title_subsection"> 2.4 Benchmarks</h3> <div class="ltx_para" id="S2.SS4.p1"> HumanEval <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib6" title="">6</a>]</cite> is a widely used benchmark for evaluating the code generation capabilities of LLMs. Evaluation on HumanEval is a convenient way to showcase the results of verified code generation to a community unfamiliar with it. For this reason, we translated the majority of the original dataset into Dafny111HumanEval dataset in Dafny: <a class="ltx_ref ltx_url" href="https://github.com/JetBrains-Research/HumanEval-Dafny/" title="">https://github.com/JetBrains-Research/HumanEval-Dafny/</a> and Nagini222HumanEval dataset in Nagini: <a class="ltx_ref ltx_url" href="https://github.com/JetBrains-Research/HumanEval-Nagini/" title="">https://github.com/JetBrains-Research/HumanEval-Nagini/</a>, 132 and 106 programs respectively. We have also contributed to a similar initiative for Verus333HumanEval-based dataset in Verus: <a class="ltx_ref ltx_url" href="https://github.com/secure-foundations/human-eval-verus" title="">https://github.com/secure-foundations/human-eval-verus</a>, which contains 55 programs as of the time of writing this paper. Not all problems from the original benchmark have been included into the datasets, partially because of time constraints, and partially because not every task is suitable for verification. For some of them, the specification duplicates the implementation (e.g. task 67), while unsupported language features are needed for others (e.g. task 2 in Dafny and task 4 in Verus). </div> <div class="ltx_para" id="S2.SS4.p2"> The Dafny and Verus benchmarks were created manually, with multiple people collaborating over several weeks. Some automation was possible at the initial stage of creating the benchmark in Nagini. For this, we modified the Dafny compiler to automatically convert the Dafny files into Nagini. Even though the verification systems resemble each other, Nagini has lower expressiveness compared with Dafny. As a result, we had to manually inspect every program and add additional invariants or adjust specifications to finish correctness proofs. </div> </section> </section> <section class="ltx_section" id="S3"> <h2 class="ltx_title ltx_title_section"> 3 Evaluation</h2> <div class="ltx_para" id="S3.p1"> In the early stages of our project, we experimented with multiple LLMs, including GPT-3.5, GPT-4o, and Claude 3 Opus. However, the quality achieved by Claude 3.5 Sonnet massively surpassed the others, leading us to rely exclusively on it since its release. Unfortunately, we have not yet run the experiments on the o1 model because of its prohibitively strict limits. Neither have we had a chance to set up the newest DeepSeek-R1 <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib12" title="">12</a>]</cite> and o3-mini <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib24" title="">24</a>]</cite> models, which promise even higher quality compared with the earlier models. In this study, we only provide the results achieved using Claude 3.5 Sonnet since it consistently demonstrated superior performance while not being too expensive in terms of time and cost. </div> <figure class="ltx_table" id="S3.T1"> <figcaption class="ltx_caption">Table 1: Percentage of verified examples for different modes and languages </figcaption> <table class="ltx_tabular ltx_centering ltx_guessed_headers ltx_align_middle" id="S3.T1.4"> <thead class="ltx_thead"> <tr class="ltx_tr" id="S3.T1.4.1.1"> <th class="ltx_td ltx_th ltx_th_column ltx_th_row ltx_border_rr" id="S3.T1.4.1.1.1"></th> <th class="ltx_td ltx_align_center ltx_th ltx_th_column ltx_th_row ltx_border_r" id="S3.T1.4.1.1.2"> <table class="ltx_tabular ltx_align_middle" id="S3.T1.4.1.1.2.1"> <tr class="ltx_tr" id="S3.T1.4.1.1.2.1.1"> <td class="ltx_td ltx_nopad_r ltx_align_center" id="S3.T1.4.1.1.2.1.1.1">Number of</td> </tr> <tr class="ltx_tr" id="S3.T1.4.1.1.2.1.2"> <td class="ltx_td ltx_nopad_r ltx_align_center" id="S3.T1.4.1.1.2.1.2.1">programs</td> </tr> </table> </th> <th class="ltx_td ltx_align_center ltx_th ltx_th_column" id="S3.T1.4.1.1.3">Mode 1</th> <th class="ltx_td ltx_align_center ltx_th ltx_th_column ltx_border_l ltx_border_r" id="S3.T1.4.1.1.4">Mode 2</th> <th class="ltx_td ltx_align_center ltx_th ltx_th_column" id="S3.T1.4.1.1.5">Mode 3</th> <th class="ltx_td ltx_align_center ltx_th ltx_th_column ltx_border_l ltx_border_r" id="S3.T1.4.1.1.6">Mode 4</th> <th class="ltx_td ltx_align_center ltx_th ltx_th_column" id="S3.T1.4.1.1.7">Mode 5</th> <th class="ltx_td ltx_align_center ltx_th ltx_th_column ltx_border_l" id="S3.T1.4.1.1.8">Mode 6</th> </tr> </thead> <tbody class="ltx_tbody"> <tr class="ltx_tr" id="S3.T1.4.2.1"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_tt" id="S3.T1.4.2.1.1">Dafny</th> <th class="ltx_td ltx_align_center ltx_th ltx_th_row ltx_border_r ltx_border_tt" id="S3.T1.4.2.1.2">132</th> <td class="ltx_td ltx_align_right ltx_border_r ltx_border_tt" id="S3.T1.4.2.1.3">113 (86%)</td> <td class="ltx_td ltx_align_right ltx_border_r ltx_border_tt" id="S3.T1.4.2.1.4">104 (79%)</td> <td class="ltx_td ltx_align_right ltx_border_r ltx_border_tt" id="S3.T1.4.2.1.5">114 (86%)</td> <td class="ltx_td ltx_align_right ltx_border_r ltx_border_tt" id="S3.T1.4.2.1.6">108 (82%)</td> <td class="ltx_td ltx_align_right ltx_border_r ltx_border_tt" id="S3.T1.4.2.1.7">80 (61%)</td> <td class="ltx_td ltx_align_right ltx_border_tt" id="S3.T1.4.2.1.8">38 (29%)</td> </tr> <tr class="ltx_tr" id="S3.T1.4.3.2"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr" id="S3.T1.4.3.2.1">Nagini</th> <th class="ltx_td ltx_align_center ltx_th ltx_th_row ltx_border_r" id="S3.T1.4.3.2.2">106</th> <td class="ltx_td ltx_align_right ltx_border_r" id="S3.T1.4.3.2.3">70 (66%)</td> <td class="ltx_td ltx_align_right ltx_border_r" id="S3.T1.4.3.2.4">57 (54%)</td> <td class="ltx_td ltx_align_right ltx_border_r" id="S3.T1.4.3.2.5">67 (63%)</td> <td class="ltx_td ltx_align_right ltx_border_r" id="S3.T1.4.3.2.6">67 (63%)</td> <td class="ltx_td ltx_align_right ltx_border_r" id="S3.T1.4.3.2.7">44 (42%)</td> <td class="ltx_td ltx_align_right" id="S3.T1.4.3.2.8">16 (15%)</td> </tr> <tr class="ltx_tr" id="S3.T1.4.4.3"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr" id="S3.T1.4.4.3.1">Verus</th> <th class="ltx_td ltx_align_center ltx_th ltx_th_row ltx_border_r" id="S3.T1.4.4.3.2">55</th> <td class="ltx_td ltx_align_right ltx_border_r" id="S3.T1.4.4.3.3">25 (45%)</td> <td class="ltx_td ltx_align_right ltx_border_r" id="S3.T1.4.4.3.4">17 (31%)</td> <td class="ltx_td ltx_align_right ltx_border_r" id="S3.T1.4.4.3.5">20 (36%)</td> <td class="ltx_td ltx_align_right ltx_border_r" id="S3.T1.4.4.3.6">22 (40%)</td> <td class="ltx_td ltx_align_right ltx_border_r" id="S3.T1.4.4.3.7">13 (24%)</td> <td class="ltx_td ltx_align_right" id="S3.T1.4.4.3.8">8 (15%)</td> </tr> </tbody> </table> </figure> <div class="ltx_para" id="S3.p2"> In the evaluation, we allowed for five iterations to be done when trying to fix verification issues. The described experiment was run on HumanEval benchmarks using Claude Sonnet 3.5 five times. We then computed the number of unique problems, verified in at least one of the runs, and gathered the statistics in Table <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S3.T1" title="Table 1 ‣ 3 Evaluation ‣ Can LLMs Enable Verification in Mainstream Programming?">1</a>. </div> <div class="ltx_para" id="S3.p3"> We can see that the performance of program synthesis in Dafny is higher than in either Nagini or Verus. This is expected given that this system is more popular than the others and there is significantly more code available among the training data. Nevertheless, the first four modes demonstrate decent results in the case of Nagini with over half of the programs successfully verified. This is not the case for Verus which is the least expressive and the newest among the three. Note that results which are not significantly higher were achieved in the AlphaVerus project <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib1" title="">1</a>]</cite> even though it features an advanced treefinement search and massively more calls to a model. </div> <div class="ltx_para" id="S3.p4"> The worst results were achieved in Mode 6, with less than 30% success rate for Dafny and 15% success rate for Nagini and Verus. We attribute this to our validation, which expects the specifications to match the ground truth. </div> <div class="ltx_para" id="S3.p5"> Finally, since our benchmarks contained different subsets of tasks from the initial dataset, we also explored the distribution of problems successfully verified in each of the languages: see Figure <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S3.F4" title="Figure 4 ‣ 3 Evaluation ‣ Can LLMs Enable Verification in Mainstream Programming?">4</a>. Notably, only a miniscule number of problems were verified only by the systems other than Dafny. This may signify that the models use their knowledge of Dafny when dealing with the others. </div> <figure class="ltx_figure" id="S3.F4"> <div class="ltx_flex_figure"> <div class="ltx_flex_cell ltx_flex_size_2"> <figure class="ltx_figure ltx_figure_panel ltx_align_center" id="S3.F4.sf1"><img alt="Refer to caption" class="ltx_graphics ltx_centering ltx_img_square" height="830" id="S3.F4.sf1.g1" src="x1.png" width="830"/> <figcaption class="ltx_caption ltx_centering">(a) Mode 1</figcaption> </figure> </div> <div class="ltx_flex_cell ltx_flex_size_2"> <figure class="ltx_figure ltx_figure_panel ltx_align_center" id="S3.F4.sf2"><img alt="Refer to caption" class="ltx_graphics ltx_centering ltx_img_square" height="830" id="S3.F4.sf2.g1" src="x2.png" width="830"/> <figcaption class="ltx_caption ltx_centering">(b) Mode 2</figcaption> </figure> </div> <div class="ltx_flex_break"></div> <div class="ltx_flex_cell ltx_flex_size_2"> <figure class="ltx_figure ltx_figure_panel ltx_align_center" id="S3.F4.sf3"><img alt="Refer to caption" class="ltx_graphics ltx_centering ltx_img_square" height="830" id="S3.F4.sf3.g1" src="x3.png" width="830"/> <figcaption class="ltx_caption ltx_centering">(c) Mode 3</figcaption> </figure> </div> <div class="ltx_flex_cell ltx_flex_size_2"> <figure class="ltx_figure ltx_figure_panel ltx_align_center" id="S3.F4.sf4"><img alt="Refer to caption" class="ltx_graphics ltx_centering ltx_img_square" height="830" id="S3.F4.sf4.g1" src="x4.png" width="830"/> <figcaption class="ltx_caption ltx_centering">(d) Mode 4</figcaption> </figure> </div> <div class="ltx_flex_break"></div> <div class="ltx_flex_cell ltx_flex_size_2"> <figure class="ltx_figure ltx_figure_panel ltx_align_center" id="S3.F4.sf5"><img alt="Refer to caption" class="ltx_graphics ltx_centering ltx_img_square" height="830" id="S3.F4.sf5.g1" src="x5.png" width="830"/> <figcaption class="ltx_caption ltx_centering">(e) Mode 5</figcaption> </figure> </div> <div class="ltx_flex_cell ltx_flex_size_2"> <figure class="ltx_figure ltx_figure_panel ltx_align_center" id="S3.F4.sf6"><img alt="Refer to caption" class="ltx_graphics ltx_centering ltx_img_square" height="830" id="S3.F4.sf6.g1" src="x6.png" width="830"/> <figcaption class="ltx_caption ltx_centering">(f) Mode 6</figcaption> </figure> </div> </div> <figcaption class="ltx_caption ltx_centering">Figure 4: Venn Diagrams showing the intersection of unique programs successfully generated in at least one of five attempts</figcaption> </figure> <figure class="ltx_table" id="S3.T2"> <figcaption class="ltx_caption ltx_centering">Table 2: Most common errors for different languages</figcaption><div class="ltx_flex_figure"> <div class="ltx_flex_cell ltx_flex_size_2"> <figure class="ltx_table ltx_figure_panel ltx_align_center" id="S3.T2.st1"> <table class="ltx_tabular ltx_centering ltx_guessed_headers ltx_align_middle" id="S3.T2.st1.2"> <thead class="ltx_thead"> <tr class="ltx_tr" id="S3.T2.st1.2.1.1"> <th class="ltx_td ltx_align_left ltx_th ltx_th_column ltx_th_row ltx_border_rr" id="S3.T2.st1.2.1.1.1">Error type</th> <th class="ltx_td ltx_align_center ltx_th ltx_th_column" id="S3.T2.st1.2.1.1.2"> <table class="ltx_tabular ltx_align_middle" id="S3.T2.st1.2.1.1.2.1"> <tr class="ltx_tr" id="S3.T2.st1.2.1.1.2.1.1"> <td class="ltx_td ltx_nopad_r ltx_align_center" id="S3.T2.st1.2.1.1.2.1.1.1">Number of</td> </tr> <tr class="ltx_tr" id="S3.T2.st1.2.1.1.2.1.2"> <td class="ltx_td ltx_nopad_r ltx_align_center" id="S3.T2.st1.2.1.1.2.1.2.1">occurrences</td> </tr> </table> </th> </tr> </thead> <tbody class="ltx_tbody"> <tr class="ltx_tr" id="S3.T2.st1.2.2.1"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_tt" id="S3.T2.st1.2.2.1.1">Invariant (maintain)</th> <td class="ltx_td ltx_align_center ltx_border_tt" id="S3.T2.st1.2.2.1.2">175</td> </tr> <tr class="ltx_tr" id="S3.T2.st1.2.3.2"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st1.2.3.2.1">Postcondition not proved</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st1.2.3.2.2">91</td> </tr> <tr class="ltx_tr" id="S3.T2.st1.2.4.3"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st1.2.4.3.1">Assertion failed</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st1.2.4.3.2">69</td> </tr> <tr class="ltx_tr" id="S3.T2.st1.2.5.4"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st1.2.5.4.1">Unresolved identifier</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st1.2.5.4.2">32</td> </tr> <tr class="ltx_tr" id="S3.T2.st1.2.6.5"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st1.2.6.5.1">Syntax error</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st1.2.6.5.2">27</td> </tr> <tr class="ltx_tr" id="S3.T2.st1.2.7.6"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st1.2.7.6.1">Invariant (entry)</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st1.2.7.6.2">17</td> </tr> </tbody> </table> <figcaption class="ltx_caption ltx_centering">(a) Dafny</figcaption> </figure> </div> <div class="ltx_flex_cell ltx_flex_size_2"> <figure class="ltx_table ltx_figure_panel ltx_align_center" id="S3.T2.st2"> <table class="ltx_tabular ltx_centering ltx_guessed_headers ltx_align_middle" id="S3.T2.st2.2"> <thead class="ltx_thead"> <tr class="ltx_tr" id="S3.T2.st2.2.1.1"> <th class="ltx_td ltx_align_left ltx_th ltx_th_column ltx_th_row ltx_border_rr" id="S3.T2.st2.2.1.1.1">Error type</th> <th class="ltx_td ltx_align_center ltx_th ltx_th_column" id="S3.T2.st2.2.1.1.2"> <table class="ltx_tabular ltx_align_middle" id="S3.T2.st2.2.1.1.2.1"> <tr class="ltx_tr" id="S3.T2.st2.2.1.1.2.1.1"> <td class="ltx_td ltx_nopad_r ltx_align_center" id="S3.T2.st2.2.1.1.2.1.1.1">Number of</td> </tr> <tr class="ltx_tr" id="S3.T2.st2.2.1.1.2.1.2"> <td class="ltx_td ltx_nopad_r ltx_align_center" id="S3.T2.st2.2.1.1.2.1.2.1">occurrences</td> </tr> </table> </th> </tr> </thead> <tbody class="ltx_tbody"> <tr class="ltx_tr" id="S3.T2.st2.2.2.1"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_tt" id="S3.T2.st2.2.2.1.1">Timeout</th> <td class="ltx_td ltx_align_center ltx_border_tt" id="S3.T2.st2.2.2.1.2">468</td> </tr> <tr class="ltx_tr" id="S3.T2.st2.2.3.2"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st2.2.3.2.1">Invariant (maintain)</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st2.2.3.2.2">259</td> </tr> <tr class="ltx_tr" id="S3.T2.st2.2.4.3"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st2.2.4.3.1">Precondition not satisfied</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st2.2.4.3.2">237</td> </tr> <tr class="ltx_tr" id="S3.T2.st2.2.5.4"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st2.2.5.4.1">Postcondition not proved</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st2.2.5.4.2">214</td> </tr> <tr class="ltx_tr" id="S3.T2.st2.2.6.5"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st2.2.6.5.1">Invariant (entry)</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st2.2.6.5.2">103</td> </tr> <tr class="ltx_tr" id="S3.T2.st2.2.7.6"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st2.2.7.6.1">Unresolved identifier</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st2.2.7.6.2">53</td> </tr> </tbody> </table> <figcaption class="ltx_caption ltx_centering">(b) Nagini</figcaption> </figure> </div> <div class="ltx_flex_break"></div> <div class="ltx_flex_cell ltx_flex_size_1"> <figure class="ltx_table ltx_figure_panel ltx_align_center" id="S3.T2.st3"> <table class="ltx_tabular ltx_centering ltx_guessed_headers ltx_align_middle" id="S3.T2.st3.2"> <thead class="ltx_thead"> <tr class="ltx_tr" id="S3.T2.st3.2.1.1"> <th class="ltx_td ltx_align_left ltx_th ltx_th_column ltx_th_row ltx_border_rr" id="S3.T2.st3.2.1.1.1">Error type</th> <th class="ltx_td ltx_align_center ltx_th ltx_th_column" id="S3.T2.st3.2.1.1.2"> <table class="ltx_tabular ltx_align_middle" id="S3.T2.st3.2.1.1.2.1"> <tr class="ltx_tr" id="S3.T2.st3.2.1.1.2.1.1"> <td class="ltx_td ltx_nopad_r ltx_align_center" id="S3.T2.st3.2.1.1.2.1.1.1">Number of</td> </tr> <tr class="ltx_tr" id="S3.T2.st3.2.1.1.2.1.2"> <td class="ltx_td ltx_nopad_r ltx_align_center" id="S3.T2.st3.2.1.1.2.1.2.1">occurrences</td> </tr> </table> </th> </tr> </thead> <tbody class="ltx_tbody"> <tr class="ltx_tr" id="S3.T2.st3.2.2.1"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_tt" id="S3.T2.st3.2.2.1.1">Type error</th> <td class="ltx_td ltx_align_center ltx_border_tt" id="S3.T2.st3.2.2.1.2">192</td> </tr> <tr class="ltx_tr" id="S3.T2.st3.2.3.2"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st3.2.3.2.1">Assertion failed</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st3.2.3.2.2">46</td> </tr> <tr class="ltx_tr" id="S3.T2.st3.2.4.3"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st3.2.4.3.1">Invariant (maintain)</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st3.2.4.3.2">28</td> </tr> <tr class="ltx_tr" id="S3.T2.st3.2.5.4"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st3.2.5.4.1">Invariant (entry)</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st3.2.5.4.2">22</td> </tr> <tr class="ltx_tr" id="S3.T2.st3.2.6.5"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st3.2.6.5.1">Syntax error</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st3.2.6.5.2">17</td> </tr> <tr class="ltx_tr" id="S3.T2.st3.2.7.6"> <th class="ltx_td ltx_align_left ltx_th ltx_th_row ltx_border_rr ltx_border_t" id="S3.T2.st3.2.7.6.1">Arithmetic underflow/overflow</th> <td class="ltx_td ltx_align_center ltx_border_t" id="S3.T2.st3.2.7.6.2">14</td> </tr> </tbody> </table> <figcaption class="ltx_caption ltx_centering">(c) Verus</figcaption> </figure> </div> </div> </figure> <section class="ltx_subsection" id="S3.SS1"> <h3 class="ltx_title ltx_title_subsection"> 3.1 Understanding Common Pitfalls</h3> <div class="ltx_para" id="S3.SS1.p1"> To better understand the problems that models face when generating code in different languages, we collected statistics about the errors reported by the verifier during 5 runs of the mode 1 on HumanEval benchmarks. We classified errors into a few groups, including syntax and type errors, unresolved identifiers, and inability to prove an invariant or a postcondition. Among all errors, timeout stands out: it does not occur as often in Dafny or Verus, since these languages are aimed at delivering results of verification quickly. Nevertheless, it is the most frequent error in the case of Nagini. As this error does not convey any meaningful information about the actual problem in the proof, LLMs rarely manage to resolve the issue. </div> <div class="ltx_para" id="S3.SS1.p2"> While the most common errors for Dafny and Nagini are caused by incomplete proofs, Verus generation suffers from type errors. Incompatible types, wrong arguments, missing type annotations are most prevalent. Such a frequent occurrence of this type of error is due to a complex type system and the fact that different types are allowed in code and in invariants. As a result, the fragment of the code in Figure <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S3.F5.sf1" title="In Figure 5 ‣ 3.1 Understanding Common Pitfalls ‣ 3 Evaluation ‣ Can LLMs Enable Verification in Mainstream Programming?">5(a)</a> leads to the error featured in Figure <a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#S3.F5.sf2" title="In Figure 5 ‣ 3.1 Understanding Common Pitfalls ‣ 3 Evaluation ‣ Can LLMs Enable Verification in Mainstream Programming?">5(b)</a>. This error can be solved by adding explicit cast to int: pos as int, but it is not often that a model is capable of it. </div> <figure class="ltx_figure" id="S3.F5"> <div class="ltx_flex_figure"> <div class="ltx_flex_cell ltx_flex_size_1"> <figure class="ltx_figure ltx_figure_panel ltx_minipage ltx_align_center ltx_align_top" id="S3.F5.sf1" style="width:433.6pt;"> <div class="ltx_listing ltx_lst_language_Dafny ltx_lstlisting ltx_listing" id="S3.F5.sf1.2"> <div class="ltx_listing_data"><a download="" href="data:text/plain;base64,Li4uCmZuIHJvbGxpbmdfbWF4KG51bWJlcnM6IFZlYzxpMzI+KSAtPiAocmVzdWx0OiBWZWM8aTMyPikKICAgIGVuc3VyZXMKICAgICAgICByZXN1bHQubGVuKCkgPT0gbnVtYmVycy5sZW4oKSwKICAgICAgICBmb3JhbGx8aTogaW50fCAwIDw9IGkgPCBudW1iZXJzLmxlbigpID09PgogICAgICAgICAgICByZXN1bHRbaV0gPT0gc2VxX21heChudW1iZXJzQC50YWtlKGkgKyAxKSksCnsKICAgIGxldCBtdXQgbWF4X3NvX2ZhciA9IGkzMjo6TUlOOwogICAgbGV0IG11dCByZXN1bHQgPSBWZWM6OndpdGhfY2FwYWNpdHkobnVtYmVycy5sZW4oKSk7CiAgICBmb3IgcG9zIGluIDAuLm51bWJlcnMubGVuKCkKICAgICAgICBpbnZhcmlhbnQKICAgICAgICAgICAgbWF4X3NvX2ZhciA9PSBpZiBwb3MgPT0gMCB7IGkzMjo6TUlOIH0KICAgICAgICAgICAgICAgIGVsc2UgeyBzZXFfbWF4KG51bWJlcnNALnRha2UocG9zKSkgfSwKICAgICAgICAgICAgcmVzdWx0LmxlbigpID09IHBvcywKICAgICAgICAgICAgZm9yYWxsfGk6IGludHwgMCA8PSBpIDwgcG9zID09PgogICAgICAgICAgICAgICAgcmVzdWx0W2ldID09IHNlcV9tYXgobnVtYmVyc0AudGFrZShpICsgMSkpLAouLi4=">⬇</a></div> <div class="ltx_listingline" id="lstnumberx99"> ... </div> <div class="ltx_listingline" id="lstnumberx100"> fn rolling_max(numbers: Vec<i32>) -> (result: Vec<i32>) </div> <div class="ltx_listingline" id="lstnumberx101"> ensures </div> <div class="ltx_listingline" id="lstnumberx102"> result.len() == numbers.len(), </div> <div class="ltx_listingline" id="lstnumberx103"> forall|i: int| 0 <= i < numbers.len() ==> </div> <div class="ltx_listingline" id="lstnumberx104"> result[i] == seq_max(numbers@.take(i + 1)), </div> <div class="ltx_listingline" id="lstnumberx105"> { </div> <div class="ltx_listingline" id="lstnumberx106"> let mut max_so_far = i32::MIN; </div> <div class="ltx_listingline" id="lstnumberx107"> let mut result = Vec::with_capacity(numbers.len()); </div> <div class="ltx_listingline" id="lstnumberx108"> for pos in 0..numbers.len() </div> <div class="ltx_listingline" id="lstnumberx109"> invariant </div> <div class="ltx_listingline" id="lstnumberx110"> max_so_far == if pos == 0 { i32::MIN } </div> <div class="ltx_listingline" id="lstnumberx111"> else { seq_max(numbers@.take(pos)) }, </div> <div class="ltx_listingline" id="lstnumberx112"> result.len() == pos, </div> <div class="ltx_listingline" id="lstnumberx113"> forall|i: int| 0 <= i < pos ==> </div> <div class="ltx_listingline" id="lstnumberx114"> result[i] == seq_max(numbers@.take(i + 1)), </div> <div class="ltx_listingline" id="lstnumberx115"> ... </div> </div> <figcaption class="ltx_caption">(a) Implementation</figcaption> </figure> </div> <div class="ltx_flex_break"></div> <div class="ltx_flex_cell ltx_flex_size_1"> <figure class="ltx_figure ltx_figure_panel ltx_minipage ltx_align_center ltx_align_top" id="S3.F5.sf2" style="width:433.6pt;"> <div class="ltx_listing ltx_lst_language_BigDafny ltx_lstlisting ltx_listing" id="S3.F5.sf2.2"> <div class="ltx_listing_data"><a download="" href="data:text/plain;base64,ZXJyb3JbRTAzMDhdOiBtaXNtYXRjaGVkIHR5cGVzCiAgLS0+IDAwOS1yb2xsaW5nX21heF8xLnJzOjI0OjgxCiAgIHwKMjYgfCBlbHNlIHsgc2VxX21heChudW1iZXJzQC50YWtlKHBvcykpIH0sCiAgIHwgICAgICAgICAgICAgICAgICAgICAgICAgLS0tLSBeXl4gZXhwZWN0ZWQgYGludGAsIGZvdW5kIGB1c2l6ZWAKICAgfCAgICAgICAgICAgICAgICAgICAgICAgICB8CiAgIHwgICAgICAgICAgICAgICAgICAgICAgICAgYXJndW1lbnRzIHRvIHRoaXMgbWV0aG9kIGFyZSBpbmNvcnJlY3QKICAgfA==">⬇</a></div> <div class="ltx_listingline" id="lstnumberx116"> error[E0308]: mismatched types </div> <div class="ltx_listingline" id="lstnumberx117"> --> 009-rolling_max_1.rs:24:81 </div> <div class="ltx_listingline" id="lstnumberx118"> | </div> <div class="ltx_listingline" id="lstnumberx119"> 26 | else { seq_max(numbers@.take(pos)) }, </div> <div class="ltx_listingline" id="lstnumberx120"> | ---- ^^^ expected ‘int‘, found ‘usize‘ </div> <div class="ltx_listingline" id="lstnumberx121"> | | </div> <div class="ltx_listingline" id="lstnumberx122"> | arguments to this method are incorrect </div> <div class="ltx_listingline" id="lstnumberx123"> | </div> </div> <figcaption class="ltx_caption">(b) Type error</figcaption> </figure> </div> </div> <figcaption class="ltx_caption ltx_centering">Figure 5: The example of Verus code, causing the type error</figcaption> </figure> <div class="ltx_para" id="S3.SS1.p3"> A more personalized approach for each types of errors could improve the quality of generated code. For instance, one can provide few-shot examples of typical errors and possible fixes for them. The Laurel project <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib22" title="">22</a>]</cite> intends to address the problem by modifying Dafny’s error messages to include more details. AutoVerus <cite class="ltx_cite ltx_citemacro_cite">[<a class="ltx_ref" href="https://arxiv.org/html/2503.14183v1#bib.bib7" title="">7</a>]</cite> proposes a rather complicated process in which unsuccessful attempts to generate proofs are collected along with the eventual correct solution to the problem. This information is then utilized in a self-debugging procedure, thus improving the quality considerably. We plan to employ these or similar methods as future work. </div> </section> </section> <section class="ltx_section" id="S4"> <h2 class="ltx_title ltx_title_section"> 4 Conclusion</h2> <div class="ltx_para" id="S4.p1"> Our study demonstrates the ability of LLMs to generate formally verified code, lowering the barriers to adoption of formal methods in mainstream programming. The high success rate in the context of Dafny motivates further research into less-explored verification systems, such as Nagini and Verus. Mistakes that LLMs tend to make for these systems likely stem from the models’ unfamiliarity with them, which we plan to address in future work by fine-tuning. This will require significantly larger datasets, the collection of which is complicated by the insufficient amount of source code published online, but can be approached through synthetic means. Another research direction can leverage specialized error-correction mechanisms and self-improving frameworks. Finally, striking the right balance between automation and human involvement can be key to making verification accessible to the wider programming community. </div> </section> <section class="ltx_bibliography" id="bib"> <h2 class="ltx_title ltx_title_bibliography">References</h2> <ul class="ltx_biblist"> <li class="ltx_bibitem" id="bib.bib1"> [1] Pranjal Aggarwal, Bryan Parno, and Sean Welleck. Alphaverus: Bootstrapping formally verified code generation through self-improving translation and treefinement. arXiv preprint arXiv:2412.06176, 2024. </li> <li class="ltx_bibitem" id="bib.bib2"> [2] Dirk Beyer, Thomas A Henzinger, Rupak Majumdar, and Andrey Rybalchenko. Path invariants. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 300–309, 2007. </li> <li class="ltx_bibitem" id="bib.bib3"> [3] Marat Boshernitsan, Roongko Doong, and Alberto Savoia. From daikon to agitator: lessons and challenges in building a commercial tool for developer testing. In Proceedings of the 2006 international symposium on Software testing and analysis, pages 169–180, 2006. </li> <li class="ltx_bibitem" id="bib.bib4"> [4] Franck Cassez, Joanne Fuller, and Aditya Asgaonkar. Formal verification of the ethereum 2.0 beacon chain. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 167–182. Springer, 2022. </li> <li class="ltx_bibitem" id="bib.bib5"> [5] Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, and Nikhil Swamy. Towards neural synthesis for smt-assisted proof-oriented programming. arXiv preprint arXiv:2405.01787, 2024. </li> <li class="ltx_bibitem" id="bib.bib6"> [6] 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. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374, 2021. </li> <li class="ltx_bibitem" id="bib.bib7"> [7] Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, et al. Automated proof generation for rust code via self-evolution. arXiv preprint arXiv:2410.15756, 2024. </li> <li class="ltx_bibitem" id="bib.bib8"> [8] Isil Dillig, Thomas Dillig, Boyang Li, and Ken McMillan. Inductive invariant generation via abductive inference. Acm Sigplan Notices, 48(10):443–456, 2013. </li> <li class="ltx_bibitem" id="bib.bib9"> [9] Marco Eilers and Peter Müller. Nagini: a static verifier for python. In Computer Aided Verification: 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I 30, pages 596–603. Springer, 2018. </li> <li class="ltx_bibitem" id="bib.bib10"> [10] Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, and Shuvendu K Lahiri. Can large language models transform natural language intent into formal method postconditions? Proceedings of the ACM on Software Engineering, 1(FSE):1889–1912, 2024. </li> <li class="ltx_bibitem" id="bib.bib11"> [11] Michael D Ernst, Jeff H Perkins, Philip J Guo, Stephen McCamant, Carlos Pacheco, Matthew S Tschantz, and Chen Xiao. The daikon system for dynamic detection of likely invariants. Science of computer programming, 69(1-3):35–45, 2007. </li> <li class="ltx_bibitem" id="bib.bib12"> [12] Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948, 2025. </li> <li class="ltx_bibitem" id="bib.bib13"> [13] Hong Hu, Zheng Leong Chua, Sendroiu Adrian, Prateek Saxena, and Zhenkai Liang. Automatic generation of <math alttext="\{" class="ltx_Math" display="inline" id="bib.bib13.1.m1.1"><semantics id="bib.bib13.1.m1.1a"><mo id="bib.bib13.1.m1.1.1" stretchy="false" xref="bib.bib13.1.m1.1.1.cmml">{</mo><annotation-xml encoding="MathML-Content" id="bib.bib13.1.m1.1b"><ci id="bib.bib13.1.m1.1.1.cmml" xref="bib.bib13.1.m1.1.1">{</ci></annotation-xml><annotation encoding="application/x-tex" id="bib.bib13.1.m1.1c">\{</annotation><annotation encoding="application/x-llamapun" id="bib.bib13.1.m1.1d">{</annotation></semantics></math>Data-Oriented<math alttext="\}" class="ltx_Math" display="inline" id="bib.bib13.2.m2.1"><semantics id="bib.bib13.2.m2.1a"><mo id="bib.bib13.2.m2.1.1" stretchy="false" xref="bib.bib13.2.m2.1.1.cmml">}</mo><annotation-xml encoding="MathML-Content" id="bib.bib13.2.m2.1b"><ci id="bib.bib13.2.m2.1.1.cmml" xref="bib.bib13.2.m2.1.1">}</ci></annotation-xml><annotation encoding="application/x-tex" id="bib.bib13.2.m2.1c">\}</annotation><annotation encoding="application/x-llamapun" id="bib.bib13.2.m2.1d">}</annotation></semantics></math> exploits. In 24th USENIX Security Symposium (USENIX Security 15), pages 177–192, 2015. </li> <li class="ltx_bibitem" id="bib.bib14"> [14] Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, and Rahul Sharma. Finding inductive loop invariants using large language models. arXiv preprint arXiv:2311.07948, 2023. </li> <li class="ltx_bibitem" id="bib.bib15"> [15] Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps. Non-linear reasoning for invariant synthesis. Proceedings of the ACM on Programming Languages, 2(POPL):1–33, 2017. </li> <li class="ltx_bibitem" id="bib.bib16"> [16] Herb Krasner. The cost of poor software quality in the us: A 2022 report. Proc. Consortium Inf. Softw. QualityTM (CISQTM), 2022. </li> <li class="ltx_bibitem" id="bib.bib17"> [17] Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying rust programs using linear ghost types. Proceedings of the ACM on Programming Languages, 7(OOPSLA1):286–315, 2023. </li> <li class="ltx_bibitem" id="bib.bib18"> [18] Ton Chanh Le, Guolong Zheng, and ThanhVu Nguyen. Sling: using dynamic analysis to infer program invariants in separation logic. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 788–801, 2019. </li> <li class="ltx_bibitem" id="bib.bib19"> [19] Yuxi Ling, Gokul Rajiv, Kiran Gopinathan, and Ilya Sergey. Sound and efficient generation of data-oriented exploits via programming language synthesis. </li> <li class="ltx_bibitem" id="bib.bib20"> [20] Hong Lu, Jiacheng Gui, Chengyi Wang, and Hao Huang. A novel data-driven approach for generating verified loop invariants. In 2020 International Symposium on Theoretical Aspects of Software Engineering (TASE), pages 9–16. IEEE, 2020. </li> <li class="ltx_bibitem" id="bib.bib21"> [21] Md Rakib Hossain Misu, Cristina V Lopes, Iris Ma, and James Noble. Towards ai-assisted synthesis of verified dafny methods. Proceedings of the ACM on Software Engineering, 1(FSE):812–835, 2024. </li> <li class="ltx_bibitem" id="bib.bib22"> [22] Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, and Yuanyuan Zhou. Laurel: Generating dafny assertions using large language models. arXiv preprint arXiv:2405.16792, 2024. </li> <li class="ltx_bibitem" id="bib.bib23"> [23] Peter Müller, Malte Schwerhoff, and Alexander J Summers. Viper: A verification infrastructure for permission-based reasoning. In Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings 17, pages 41–62. Springer, 2016. </li> <li class="ltx_bibitem" id="bib.bib24"> [24] OpenAI. Openai o3-mini system card. 2025. </li> <li class="ltx_bibitem" id="bib.bib25"> [25] Gabriel Poesia, Chloe Loughridge, and Nada Amin. dafny-annotator: Ai-assisted verification of dafny programs. arXiv preprint arXiv:2411.15143, 2024. </li> <li class="ltx_bibitem" id="bib.bib26"> [26] Daniel Riley and Grigory Fedyukovich. Multi-phase invariant synthesis. In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 607–619, 2022. </li> <li class="ltx_bibitem" id="bib.bib27"> [27] Álvaro F Silva, Alexandra Mendes, and João F Ferreira. Leveraging large language models to boost dafny’s developers productivity. In Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE), pages 138–142, 2024. </li> <li class="ltx_bibitem" id="bib.bib28"> [28] Jean Souyris. Industrial use of compcert on a safety-critical software product. <a class="ltx_ref ltx_url" href="https://projects.laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris.pdf" title="">https://projects.laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris.pdf</a>, 2014. </li> <li class="ltx_bibitem" id="bib.bib29"> [29] Akhilesh Srikanth, Burak Sahin, and William R Harris. Complexity verification using guided theorem enumeration. ACM SIGPLAN Notices, 52(1):639–652, 2017. </li> <li class="ltx_bibitem" id="bib.bib30"> [30] Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. Clover: Closed-loop verifiable code generation. In International Symposium on AI Verification, pages 134–155. Springer, 2024. </li> <li class="ltx_bibitem" id="bib.bib31"> [31] Jianan Yao, Ziqiao Zhou, Weiteng Chen, and Weidong Cui. Leveraging large language models for automated proof synthesis in rust. arXiv preprint arXiv:2311.03739, 2023. </li> <li class="ltx_bibitem" id="bib.bib32"> [32] David Young, Ziyi Yang, Ilya Sergey, and Alex Potanin. Higher-order specifications for deductive synthesis of programs with pointers. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2024. </li> <li class="ltx_bibitem" id="bib.bib33"> [33] Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. Hacl*: A verified modern cryptographic library. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pages 1789–1806, 2017. </li> </ul> </section> <div class="ltx_pagination ltx_role_newpage"></div> </article> </div> <footer class="ltx_page_footer"> <div class="ltx_page_logo">Generated on Tue Mar 18 11:56:05 2025 by <a class="ltx_LaTeXML_logo" href="http://dlmf.nist.gov/LaTeXML/">LaTeXML<img alt="Mascot Sammy" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAsAAAAOCAYAAAD5YeaVAAAAAXNSR0IArs4c6QAAAAZiS0dEAP8A/wD/oL2nkwAAAAlwSFlzAAALEwAACxMBAJqcGAAAAAd0SU1FB9wKExQZLWTEaOUAAAAddEVYdENvbW1lbnQAQ3JlYXRlZCB3aXRoIFRoZSBHSU1Q72QlbgAAAdpJREFUKM9tkL+L2nAARz9fPZNCKFapUn8kyI0e4iRHSR1Kb8ng0lJw6FYHFwv2LwhOpcWxTjeUunYqOmqd6hEoRDhtDWdA8ApRYsSUCDHNt5ul13vz4w0vWCgUnnEc975arX6ORqN3VqtVZbfbTQC4uEHANM3jSqXymFI6yWazP2KxWAXAL9zCUa1Wy2tXVxheKA9YNoR8Pt+aTqe4FVVVvz05O6MBhqUIBGk8Hn8HAOVy+T+XLJfLS4ZhTiRJgqIoVBRFIoric47jPnmeB1mW/9rr9ZpSSn3Lsmir1fJZlqWlUonKsvwWwD8ymc/nXwVBeLjf7xEKhdBut9Hr9WgmkyGEkJwsy5eHG5vN5g0AKIoCAEgkEkin0wQAfN9/cXPdheu6P33fBwB4ngcAcByHJpPJl+fn54mD3Gg0NrquXxeLRQAAwzAYj8cwTZPwPH9/sVg8PXweDAauqqr2cDjEer1GJBLBZDJBs9mE4zjwfZ85lAGg2+06hmGgXq+j3+/DsixYlgVN03a9Xu8jgCNCyIegIAgx13Vfd7vdu+FweG8YRkjXdWy329+dTgeSJD3ieZ7RNO0VAXAPwDEAO5VKndi2fWrb9jWl9Esul6PZbDY9Go1OZ7PZ9z/lyuD3OozU2wAAAABJRU5ErkJggg=="/></a> </div></footer> </div> </body> </html>