DafnyBench: A Benchmark for Formal Software Verification
Authors: Chloe R Loughridge
Qinyi Sun
Seth Ahrenbach
Federico Cassano
Chuyue Sun
Ying Sheng
Anish Mudide
Md Rakib Hossain Misu
Nada Amin
Max Tegmark
Venue: Accepted by TMLR ()

Abstract: We introduce DafnyBench, the largest benchmark of its kind for training and evaluating machine learning systems for formal software verification. We test the ability of LLMs such as GPT-4 and Claude 3 to auto-generate enough annotations for the Dafny formal verification engine to successfully verify over 750 programs with about 53,000 lines of code. The best model and prompting scheme achieved 68% success rate, and we quantify how this rate improves when retrying with error message feedback and how it deteriorates with the amount of required code and annotations. We hope that DafnyBench will enable rapid improvements from this baseline as LLMs and verification techniques grow in quality.

Published in Transactions Machine Learning Research (01/2025)
DafnyBench: A Benchmark for Formal Software Verifi- cation
Chloe Loughridge" Harvord College
cloghhrigeBBoolegghhaaad.. edu
Qinyi Sun*t Massachusetts Institute of Technology
wendysuu @riil. edu
Seth Ahrenbach
seth reth.ahrenbachh@@omnfeeeeee
Federico Cassano
cassono.f@horlleasserr.cco edu
Northeastern Universily
Chuyue Sun Stanford University
chaynes@sstanoord.co edu
Ying Sheng Stanford Universily
gingg1120@ssnm/ord..dd
Anish Mudide
amadide &mmit. edu
Massachusetts Institute of Technology
Md Rakib Hossain Misu Universily of California Irvine
mdrlo@uuii edu.
Nada Amin Harvord University
Sommnn@ens.harsune edu
Max Tegmark
Legmork Comeerkkmmml.oom edu
Massaclussells Instilute of Technology
Reviewed on OpenReview: https: // openreveew. net/ forum? TWWcc
Abstract
We introduce Dafny the largest benchmark of its kind for training and evaluating machine learning systems for formal software verification. We test the ability of LLMs such as GPTT4 and Claude 3 to auto-generate enough annotations for the Dafny formal verification engine to successfully verify over 750 programs with about 53,000 lines of code. The best model and prompting scheme achieved 68% success rate, and we quantify how this rate improves when retrying with error message feedback and how it deteriorates with the amount of required code and

---

Published in Transactions Machine Learning Research (01/2025)
annotations. We hope that DafnyBench will enable rapid improvements from this baseline LLMs and verification techniques grow in quality.
1 Introduction
Rapidly improving Large Language Models (LLMs) Bubeck et al. (2023); Authropic 2024 Team et al. 2023 are helping accelerate software development through co-pilots and other program synthesis tools. But how can we ensure that LLM-generated code meets our specifications and reliably does precisely what it is supposed to do? Indeed, this remains a persistent problem even with human-written code: major codc-testing efforts failed to prevent c.g. bugs causing an Ariano-V rocket explosion European Space Agency/ (1996) and embarrassing security vulnerabilities ssh Heartbleed 2024) and the Bash shell Wikipedia contributors (2024b). The latter was built into the Unix operating system for 25 years before being discovered.
Although formal veriftcation can guarantee perfect reliability, providing rigorous mathernatical proof that software meets specification, it has yet to gain widespread adoption because it is costly. Formally verifying code is often significant burden on the developer (Huang et al. 2024 Orenes- Vera et al. tools tend to involve a major learning curve above and beyond just learning code, greatly reducing the pool of people able to do this work.
2023 Moreover, existing
Machine learning methods have the potential to minimize common pain point of formal methods, ie., writing and verifying formal specifications. There is growing body of work that demonstrates the effectiveness of L.LMs on the analogous problem of automated theorem proving. In this related setting, AI produces formal proofs not about code but about mathematical thcorems. Fueled by the advent of benchmarks totaling over 100,000 theorems, AI lools have during the past few years improved their proof success fraction to over 82% (Polu & Sutskever 2020 Lample et al.) 2022)
Unfortunately, formal verification sorely lacks correspondingly large benchmarks: the largest of their kind Clover (Sun et al., 2024) and dafny-synlhesis (Misu al. 2024)), containing 66 and 153 programs, respectively. There is room for expanding not only their size, but also their level of difficulty: For example, Clover is limited to
programs, and sometimes the formal specification for the program directly repeats the implementation of the algorithm (see Appendix G To support automation of formal verification, the goal of the present paper is to provide such a benchmark expansion. We do so by assembling a suite of formally verified programs written in Dafay, a formal verification language that was developed for easy adoption by programmers due to its similarity with popular imperative programming languages such Python and C++ [Leino) 2023 In order for formal verification to succeed, most of these programs require supplementary Lext constiluting "annolations" lo the automated theorem prover.
The rest of this paper is organized as follows. We summarize related work in Section 2 describe our benchmark construction in Section g and quantify the ability of current LLMs to solve benchmark verification Lasks Section 4 We summarize our results and discuss promising opportunities for further work in Section We provide further details on the benchmark construction and evaluation in appendiccs.
2

---

Published in Transactions Machine Learning Research (01/2025)
2
Related Work
The verification of software systems relies variety of approaches and frameworks, For proving full correctness, Hoare logic represents one of the most widespread formal frameworks (Huang et al. 2024 To prove the full correctness of a program using Hoare logic, one must give a specification for a program. Consider the program LinearSearch (A, P), which finds the first element in the array with some property P. The specification for this program consists of an optional precondition which property of x in its original state, at the time of the function call- and a postcondition, which expresses a property of the program's result. In Figure 1 define multiple postconditions for LinearSearch by using ensures statements this function will be within the array bounds of A, (line 3) the value in A[n] has the desired property P and otherwise is set to the length of A, (line 4) n is the first index at which P applies in the array A. We call this combination of precondition(s) and postcondition(s: the specification of the program. Verifying the program means proving that the implementation of the program matches its specification. Leino et al have designed a language for writing formally verifiable code, called Dafny (Leino) 2023), and this is the language in which we have written LinearSearch in Figure) In Dafny, programmer declares specifications for methods using ensures and requires clauses. Programs in Dafny will only compile if an underlying SMT solver find proof showing that the program implementation matches its specification. Often the SMT solver requires additional annotations, like loop invariants and assert statements in the body of the program, to find proof linking the program implementation to its specification.
lines 2-4: (line 2) the returned index value from
method LinearSearch (T> array<T>, P: T >> bool) returns (n: int)
ensures 0 <= n <= Length ensures == Length Il P(ann))
ensures forall i :: < eiiinn => (P(a[a))
while !- Length
invariant
<= Length
invarient forall
(P(a(i))
if (((nn)) }
} return:
:
Figure 1: An example ground_trute program that fully verified with Dafny. To create the hall_verificatin, c lask, we would remove the invariant lines from the program above.
As summarized in Table [ below, there is a striking lack of training data for formal verification: while there are hundrods of thousands of training examples for proving mathematical theorems and over ten thousand training examples for synthesizing programs, there far less training data for formal verification for example, there are only 66 + 153 219 for proving program correctness in the Dafny language. This motivates work in the current paper to expand
3

---

Published in Transactions Machine Learning Research (01/2025)
the benchmarks from Clover and dafuy-synthesis and build DafnyBench. Mathematical theorem proving datascts focus logical reasoning, but are disconnected from real-world programming applications. DafnyBench, as formal verification benchmark, tests model's capabilities in both formal reasoning and programming. Program synthesis benchmarks usually ask a model to generate code from specifications or descriptions of what the code is supposed to achieve, but they lack the correctness guarantee that verifies the generated code is correct. In contrast, DafnyBench asks a model to generate annotations from specifications and code, where "annotations" are supplementary text that can help Dafny verifier prove that property claimed to be true indeed true.
Summary of popular machine-learning benchmark datasets for proving mathematical theorems, synthesizing programs, and formally verifying programs. Size is mcasured by the number of samples in each dalaset. In the formal reasoning dalasels, each sample is usually math problem or theorem. In the program synthesis and verified software programming benchmarks, each sample corresponds to a program.
Table 1:
Category
Dataset
Size
CoqGym Yang & Deng 2019
71,000 proofs
LeanDojo Yang et al. 2023
98,734 proofs
Mathematical theorem proving
PISA (pis) 2021
138,000 proofs
Natural Proofs Welleckk et al.
2021
15,000 proofs
Archive of Formal Prools Blanchette et al.
2015
million lines of code
APPS Hendrycks al. HimanFvalx (Zheng et al.
2021
10,000 programs
2023b
Chen et al. 2021
165 programs
Unverified program synthesis
MBPP Austin et al. 2021
974 programs
SWEBench (Jimenez ct al.
2023
2, 2,294 programs
LiveCodeBench (Jain et al.
2024
grows weekly
Formal software verification
Clover Sun et al.
2024)
66 programs
Dafny-synthesis [Misu et al.
2024]
153 programs
The 66 programs in the Clover benchmark are human Human-written. In contrast, dafny--yytheeiis translates 153 MBPP problems from Python to Dafny using GPT-4. While this method is more efficient than manual translation, it could potentially skew the distribution of represented problems away from real-world Dafny problems that may be too hard for GPT-4 to verify on its own (Misu et al.) (024).. Our dataset counterbalances this potentially skewed distribution by introducing problems verified by human programmers GitHub.
Clover proposes the most sophisticated benchmark evaluation strategy to date for formally verifiable software: the authors suggest a six-way consistency check between code, docstrings, and annotations. We do not yet implement the full Clover evaluation schome Dafny and instead deem a benchmark program "solved" if a model can make pass the Dafny verifier without modifying the requires and ensures statements in the program and without using (iverify false] or assume false (sce Appendix F for further details).
4

---

Published in Transactions Machine Learning Research (01/2025)
3 DafnyBench Construction
3.1 Sourcing Ground Truth Programs
In total, our DafnyBench benchmark contains 782 ground_ truth stand-alone Dafny programs that compile. These problems come from the following sources:
GitHub Scrape: We scraped all publicly available Dafny files on GitHub published on the before the end of 2023. The relevant. files were returned from the Git API using the language Dafny search command. We adapted deduplication script from (Mou et all 2023 to retain unique set of scraped Dafny files from Github. The de-duplication process reduced the number of .dff files from ~15,000 to ~5,000. We then attempled to verify each of these remaining files using the dafny verify command with local installation of Dafuy 4.3.0, and removed any files that did not verify. At this stage, we removed all of the files from the Clover repository Sun et al. (2024), which had already been formatted as benchmark files. This left. 1,112 files. We found that 374 of these files lacked ensures statements, and 459 of lacked assert and invariant clauses. We removed the union of these sets, which left us with 556 ground Soound truth files. Out of these files, 113 verify without any compiler annotations. To mitigate data contamination, models should ideally not be trained on data from the repositories listed in Appendix E
our benchmark
We added 62 ground truth textbook Dafny programs provided by the Clover dataset (Sun et al. 2024 We formatted these to fit our benchmark style and removed their compiler annotations. Out of these files, 23 verify without any compiler annotations.
Clover:
Dafny-synthesis: Finally, we included 164 Dafuy programs provided by the dafry-synthesis benchmark. These problems have been translated from the MBPP benchmark (Misu al. 2024). Out of these files, 72 verify without any compiler annotations.
The ground_ truth programs in our dataset have on average 2.04 methods, 0.98 functions, and 1.31 lemmas. This places the mean complexity of our examples at a level higher than Clover alone, which has only one stand-alone method per example.
3.2 Task Design: Fill Annotations
DafnyBende evaluates LLMs on the fill annotations task. For this task, we took a ground truth program, removed all of its annotations (i.e., all of the assert and invariant statements the body of the code), and asked LLM to fill annotations back in so that the resulting program could be verified with Dafny.
We do not demarcate from where these annotations have been removed, i.c., we do not insert /* TODO */ after we remove each annolation, which would make the task easier and not reflective of models utility in real-world use cases.
In the context of our rumning example the LinearSearch program from Figure completing the loop invariants or some equivalent phrasing of them- on lines 8 and Without these loop invariants, the program will not compile because Dafny cannot find proof that it matches its specification.
fill_annorl annotations lask would mean adding back the
5

---

Published in Transactions Machine Learning Research (01/2025)
Meai: 2.04
Mean; 0.98
Nean: 1.31
Frequancc
Frequenccy
Frequeency
Methods
Lemmas
(a)
(b)
(c)
1916.47
Mean:
Median: 866 50
Median: 132. 22.00
Frequeency
Cheracters
Annotetion characters
(d)
(e)
Figure 2: Distributions of method (a), function (b), lemma (c), character (d), annotation character
(e) counts Dafny Bench.
Evaluation Metric An LLM's attempt to fill annotations back in for a test program counted as a success if all following conditions are satisfied: 1) The reconstructed program is verified with Dafny; 2) LLM preserves all preconditions (requires statements) and postconditions (ensures statements); and 3) LLM does not use {:verify false} fassume false} to "cheat."
4 Experiments
In this section, report success rates for different models on the anllaaonttaionns task, well as provide some insight into current LLMs' capabilities at writing annotations for formal verification.
4.1 Prompts & Hyperparameters
We tried to keep prompts and hyperparameters mostly the same across models in order to reduce the difference between model performances that caused by hyperparameters. However, the prompts are not fully identical. For example, when we ask LLM simply return the annotations- filled program without any explanation, Claude tends to add explanations that interfere with Dafny compilation. Thus, we had to adjust some prompts slightly to fit each model's peculiarities.
For hyperparameters, we set max Lax_tokens- = 4096, which corresponds to the lowest max output token limit among all the evaluated models, and we set temperature = 0.3. We gave each model up to n = 10 attempts at a given file. If it succcoded on an attempt before the th it would be carly stopped. If the model failed on any of the intermediatte atlempls, received the Dafny error message and was asked fill in the annotations again with the error message taken into consideration. it failed all attempts, it was considered to fail that specific test program.
6

---

Published in Transactions Machine Learning Research (01/2025)
Test generation: Remove annotations from ground truth
nethod
returns
method returns
requires ... ensures
irecondition
requires ...
ttoon // Postcondl ton
// Pos testtonddttee
ensures
// Cade bady assert
!! Code bedy w/o annota Lans
...
1/
// Annotat:on
LLM reconstructs annotations
Verify reconstructed program with Dafny
nethod
returns
recuires ensures
Precondction
Dafny
Postcondiiton
Code: budy invariant assert
Anrotation reconstruc Anrotation recons truc ted
X
Figure 3: Overview evaluating LLM on a Dafny Bench test program.
4.2 Basic Results
We tested GPT-4o, GPT-4 Turbo OpenAl et al. 22024 GPT--355 Turbo Brown al. (0200), Claude 3 Opus Anthropic (024)) and CodeLlama- Losinaa--b-maee Instruct--f hug (2022) on the 292-program benchmark. Table shows that Claude Opus performed best, achieving a success rate ~ 68%.
4.3 Difficulty Utilizing Dafny Error Messages
Figure shows how the cumulative success rate improved with more attempts n. We see that the best models succeeded on the first. try about 54%, with rapidly diminishing returns after that, approaching plateau about 65% for n This suggests that the LLMs are not great at taking Dafny error messages into considcration, struggle to cope with the underlying task.
7

---

Published in Transactions Machine Learning Research (01/2025)
80%
Model
% Success
GPT-40
70%
GPT-4-turbo
No LLM
26.9
GPT-3.5-turbo
GPT-3.5 Turbo
44.0 1.8
60%
CodeLlema-7b
Claude-3-Opus
GPT-4 Turbo
59.8 1.8
50%
GPT-4o
59.3 1.8
Success
40%
Claude Opus
67.8 1.7
30%
gadeelamaa-7-Insttrutta
28.0 + 1.6
20%
Table 2: Models' success rates at writing annotations for DafuyBench, with = 10 attempts given. Dafuy succeeds in auto- verifying some programs even without an- notations, corresponding the "No LLM" 26.9% success rale baseline.
10%
0%
# of attempts given
Figure Success rate vs. number of attempls given.
4.4 Difficulty Grows with Program Size & Annotation Quantity
Figure 58 show that the success rale drops with program size. An obvious explanation could be that there is more to verify and more annotations needed. Also, as program gets longer, there may be more dependencies among variables, functions, methods, and classes, increasing the overall verification difficulty level.
Figure 5b shows that the success rate drops with the annotation quantity, defined as the number of characters in the lines of compiler annotations. In other words, the success rate drops with the amount of work that the LLM needs to do (the amount of text that it needs to insert in the right places).
4.5 Models' Common Failure Types
To analyze where LLMs failed on the benchmark, categorized failures into nine types, including verification logic error, code logic error, type error, resolution error, syntax issue, altered specification, timeout, trivial verification, and others. For a test program that a model failed at, we: 1) checked for timeout, cheating by altering specification, and cheating by trivial verification; and 2) passed Dafny error message from the failed program to Claude and asked it to classify the failure type.
Table 3 explains each failure type, and Figure gives by-model statistics of failure types.
5
Discussion & Conclusions
We have assembled the largest machine learning benchmark date for formal software verification and made publicly available on GitHub at https://anonymouse 4open /ccee//ccccceetttaaafyyiiinc
5.1
Opportunities for Larger Benchmarks
will be valuable to further expand formal verification benchmarks, which still remain more than two orders of magnitude smaller than corresponding benchmarks for mathematical theorem proving.
8

---

Published in Transactions Machine Learning Research (01/2025)
100%
100%
GPT-40
GPT-4-turba
GPT-4-turbo
GPT-3.5-turbo
GPT-3.5-turb
Claude-3-Opus
Claude-3-Opus
Success rate
CodeLlame-70
Success rate
CodeLlama-7b
0%
1000
10k
100
1000
Program length (characters)
Annotation quantity (characters)
(a)
(b)
Figure 5: Mean success rate of each bin vs. program length (a), and mean success rate of each bin annotation quantity (b). The vertical lines indicate the bin boundaries used, where the bins have an almost uniform distribution of the programs. Note that the bins are different for the two metrics. For better visual clarity, the scales are adjusted for both plots and their z-axes do not start at 0 character.
Table 3: Examples of failure types. Note that the examples are samples, not complete list, for each failure type.
Failure Type
Examples
Code logic error Verification logic error
Index out of range Target object might be mull
Cannot prove termination / Assertion might not hold
Syntax issue
Ibrace/rbrace expected Semicolon expected / Unresolved identifier Value does not satisfy the subset constraints of 'nat" Boogic program had... resolution crrors Verification timcout
Type eгror
Resolution error
Timeout
Trivial verification
Cheating by using {iverify false} or assume false
Altered specification
Cheating by altering provided specification
Other
Failure type not belonging to any listed category above
One convenient way to expand the number of available problems may involve incorporating Dafny prograis from GitHub that have dependencies spread across multiple files (while Dalny Bench encompasses increasingly complex multi-step programs, its programs each fit in a single file, avoiding the intricacios associated with distributed files or the integration of external librarics).
Perhaps models that perform especially well on this initial benchmark can later be used to expand it by translating existing Python benchmark problems into Dafny, Rust Klabnik & Carol Nichols 2021 other popular formal verification languages.

---

Published in Transactions Machine Learning Research (01/2025)
Failure type
verification eetrrattiooooiieerree _loiiceerror
500
altered_ specss
syntax_isat issue
Count
400
gode_logic_erm
timeout
type_error
other
resolution,
100
ieriia_vvriiiiatiion
claude-3-opus
gpt-4o
gpt-4-turbo
gpt-3.5-turbo
codellama-7b
Model
Figure 6: Counts of failures by failure type and by model. Note that model could have multiple failures for single test program (for example, it might have both verification logic error and synlax issue). Also note that the closed-source models had most of their failures al verification logic, while the open-source model had most of its failures at syntax issues and cheating by altering specification.
A subset of the programs we scraped from GitHub do not have appropriate docstrings. By building a benchmark with better code documentation, models may be able to leverage helpful contextual information to better constructing verification annotations.
5.2 Benchmark Evaluation Limitations
Data contamination emerges as a potentially significant. limitation for evaluating LLMs on Dafny- Bench. Scraping data from platforms such as GitHub introduces risks of leveraging previous models' training data into the benchmark evaluation, potentially inflating the abilities of certain models. To help relieve this concern, future work can augment the programs in DafnyBench by doing program transformations (e-g.; by changing variable names in the programs, adding spurious code blocks, and changing order of lines that do not depend each other), expand the dataset by asking LLMs that good at Dafny or fine-tuned on datasets like DafnyBench generate synthetic data.
Another limitation emerges in that Bench does not assess model's competence in translating natural language into concise formal specifications. Arguably, this conversion is a demanding and crucial skill we seek from language models: the capacity to validate, beyond merely verifying code. The pivotal question is whether a model can assist in identifying the essential properties an algorithm must fulfill. This provides exciting frontier for future work, which we begin to brainstorm in Appendix B
5.3 Opportunities for Improved LLM Results
We evaluated the models with a fixed lemperature setting and max output token limit of 4096, and we used prompts that were manually but not very systematically tuned for effectiveness (see Appendix A all of those choices probably leave room for improvement.
10

---

Published in Transactions Machine Learning Research (01/2025)
We do not yet provide an official training dataset or models custom-trained do well on the DafuyBench ovaluation set. However, do provide the full json file producod by the GitHub scrape, and we separately provide the names of the files use for the evaluation benchmark. Hence, it is possible for researchers to use files from the Github scrape that are not used in the benchmark as training data, though we cannot at this time provide strong guarantees on similarity between such training problems and the benchmark problems.
We also see opportunities for LLM-related innovation on the algorithmic side: out-of-the-box LLMs provide a floor but not ceiling for possible performance this benchmark. For example, fine-tuning search- based inference-time algorithms might boost models' performances this benchmark
Brandfonbrener et al. 2023
5.4 The Potential of Better LLM-Pooered Verifiers
LLMs also have potential to improve formal verification in more profound ways than mentioned above, when used in combination with other AI tools. For example, they can help automate the identification of sub-goals and annolations, reducing the search space for automated theorem provers and SAT solvers. A software developer is likely able to specify the high level assurance properties of a piece code, but may lack familiarity with the complexities of proof sub-goals and annotations. LLMs offer way to bridge this gap between software developers and formal verification.
Bigger, more general benchmarks can be used to train LLMs to specify sub-goals and annotations in formats most useful to the presently available provers and solvers. Benchmarks covering broad ground, from cryptography, lambda calculus, embedded systems, and aviomics, in a variety of widely used programming languages suitable for verification, will help create LLMs that can take real-world software, automatically process and serve it to verification tools, and inform the developer in near real time about the correctness of the code. The problem is analogous automated theorem provers and model checkers in the domain of mathematics. For a survey on the application of deep learning to automated thcorem proving, see Li et al. 2024).
that solved by existing
For further discussion on LLM's potential for auto-verilying program synthesis, see Appendix C
References
Pisa: Isabelle proofs dataset.
2021.
Code llama: Fine-tuning Ilama for code generation.
http:://higgingfacecco/////
Hhind-CodeLlama 34B-v2 2022.
Anthropic. The claude 3 model family: Opus, sonnet, haiku. Technical report, Authropic, 2024.
Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carric Cai, Michael Terry, Quoc Le, and Charles Sutton. Program synthesis with large language models, 2021.
Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, and Tobias Nipkow. Mining the archive of formal proofs. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge (eds.), Intelligent Computer Mathematics, pp. 3 17, Cham, 2015. Springer International Publishing. ISBN 978-3-319-20615-8.
11

---

Published in Transactions Machine Learning Research (01/2025)
David Brandfonbrener, Sibi Raja, Tarun Prasad, Chloe Loughridge, Federico Cassano, Jianang Yang, Simon Henniger, William E. Byrd, Robert Zinkov, and Nada Amin. Verified multi-step synthesis using large language models and monte carlo tree search, 2023.
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert- Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, 1lya Sutskever, and Dario Amodei. Language models are few-shot learners, 2020.
Sébastien Bubeck, Varun Chandrasekaran Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Kamar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, et al. Sparks of artificial general intelligence: Early experiments with gpt-4. arXiv preprint orXiv:2003. 12712, 2023.
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, 2021.
Design Automation Standards Committee and Automatic Test Program Generation Subcommittee. Ieee standard for vhdl language reference manual. IEEE Std 1076-2019, pp. 1-673, 2019. doi: 10. 10.1109/EFFRSTD. 2D0.TDD2211000 2019.8938196.
European Space Agency. Flight 501 failure, 1996. URL https://esamulliieddiaa esa. int int/docs/ esa-x-1819eng pdf
Accessod: 2024-06-04.
Heartbleed. The heartbleed bug. https://heartbleedd.cm
2024. Accessed: 2024-06-04.
Dan Hendrycks, Steven Basart, Saurav Kadavath, Mantas Mazeika, Akul Arora, Ethan Guo, Collin Burns, Samir Puranik, Horace He, Dawn Song, and Jacob Steinhardt. Measuring coding challenge competence with apps. arXiv preprint 1=Xi::2155009933 2021.
Li Huang, Sophie Ebersold, Alexander Koglenkov, Bertrand Meyer, and Yinling Liu. Lessons from formally verified deployed software systems (extended version), 2024. URL abs/2301.0220
Naman Jain, King Han, Alex Gu, Wen-Ding Li, Fanjia Yan, Tianjun Zhang, Sida Wang, Armando Solar-Lezama, Koushik Sen, and Ion Stoica. Livecodebench: Holistic and contamination free evaluation of large language models for code. arXiv preprint, 2024.
Carlos F. Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, Karthik Narasimhan, et al. Swe-bench: Can language models resolve real-world github issues?, 2023.
Steve Klabnik and with contributions from the Rust Community Carol Nichols. The Rust Pro- gramaning Language. No Starch Press, second edition, 2021. URL http:://doccruuutttee org/
stable/book/
Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayal, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. HyperTree Proof Search for Neural Theorem Proving. arXiv, May 2022. doi:
12

---

Published in Transactions Machine Learning Research (01/2025)
K Rustan M Leino. Program Proofs, MIT Press, 2023.
Xun Li, Mohit Tiwari, Jason K. Oberg, Vineeth Kashyap, Frederic T. Chong, Timothy Sherwood, and Ben Hardekopf. Caisson: & hardware description language for secure information flow. In Proceedings of the 32nd ACM SIGPLAN Conference on Progromming Language Design and Implementation, PLDI '11, pp. 109-120, 120, New York, NY, USA, 2011. Association for Computing Machinery. ISBN 9781450006638. doi: 01444/5199999811999 1145/1993498. 1993512
URL https:://oi. org/10
Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving. arXiv preprint arXiv:2404.0900 2024.
Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, and James Noble. Towards ai-assisted synthesis of verified dafny methods. Proc. ACM Softu. Eng., (FFE), 2024. doi: 10.1145/364333 URL
https://doi... 2trg//o.11 1144/3643766
Chenghao Mou, Chris Ha, Kenneth Enevoldsen, and Peiyuan Liu. Reference snapshot, September 2023. URL https://doi org/10 wtgg/...//1..... w281/22eooooo..... 8364980
OpenAI, Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, Red Avila, Igor Babuschkin, Suchir Balaji, Valerie Balcom, Paul Baltescu, Haiming Bao, Mohammad Bavarian, Jeff Belgum, Irwan Bello, Jake Berdine, Gabriel Bernadett-Shhpirg. Christopher Berner, Lenny BogdonofT, Oleg Boiko, Madelaine Boyd, Anna-Tauss Brakman, Greg Brockman, Tim Brooks, Miles Brundage, Kevin Button, Trevor Cai, Rosie Campbell, Andrew Cann, Brittany Carey, Chelsea Carlson, Rory Carmichael, Brooke Chan, Che Chang, Fotis Chantzis, Derek Chen, Sully Chen, Ruby Chen, Jason Chen, Mark Chen, Ben Chess, Chester Cho, Casey Chu, Hyung Won Chung, Dave Cummings, Jeremiah Currier, Yunxing Dai, Cory Decarcaux, Thomas Degry, Noah Deutsch, Damicn Deville, Arka Dhar, David Dohan, Steve Dowling, Sheila Dunning, Adricn Ecoffct, Atyy Eleti, Tyna Eloundou, David Farhi, Liam Fedus, Niko Felix, Simón Posada Fishman, Juston Forte, Isabella Fulford, Leo Gao, Elie Georges, Christian Gibson, Vik Goel, Tarun Gogineni, Gabricl Goh, Rapha Gontijo-Lopes, Jonathan Gordon, Morgan Grafstein, Scott Gray, Ryan Greene, Joshua Gross, Shixiang Shane Gu, Yufei Guo, Chris Hallacy, Jesse Han, Jeff Harris, Yuchen He, Mike Heaton, Johannes Heidecke, Chris Hesse, Alan Hickey, Wade Hickey, Peter Hoeschele, Brandon Houghton, Kenny Hsu, Shengli Hu, Xin Hu, Joost Huizinga, Shantanu Jain, Shawn Jain, Joanne Jang, Angela Jiang, Roger Jiang, Haozhun Jin, Denny Jin, Shino Jomoto, Billie Jonn, Heewoo Jun, Tomer Kaftan, Lukasz Kaiser, Ali Kamali, Ingmar Kanitscheider, Nitish Shirish Keskar, Tabarak Khan, Logan Kilpatrick, Jong Wook Kim, Christina Kim, Yongjik Kim, Jan Hendrik Kirchner, Jamie Kiros, Matt Knight, Daniel Kokotajlo, Lukasz Kondraciuk, Andrew Kondrich, Aris Konstantinidis, Kyle Kosic, Gretchen Krueger, Vishal Kuo, Michael Lampe, Ikai Lan, Teddy Lee, Jan Leike, Jade Leung, Daniel Levy, Chak Ming Li, Rachel Lim, Molly Lin, Stephanie Lin, Mateusz Litwin, Theresa Lopez, Ryan Lowe, Patricia Lue, Anna Makanju, Kim Malfacini, Sam Manning, Todor Markov, Yaniv Markovski, Bianca Martin, Katie Mayer, Andrew Mayne, Bob McGrew, Scott Mayer McKinney, Christine McLeavey, Paul McMillan, Jake McNeil, David Medina, Aalok Mchta, Jacob Menick, Luke Motz, Andrey Mishchenko, Pamela Mishkin, Vinnie Monaco, Evan Morikawa, Daniel Mossing, Tong Mu, Mira Murati, Oleg Murk, David Mély, Ashvin Nair, Relichrr Nakano, Rajeev Nayak, Arvind Neelakantan, Richard Ngo, Hyconwoo Noh, Long Ouyang, Cullen O'Keefe, Jakub Pachocki, Alex Paino, Joe Palermo, Ashley
13

---

Adam Procter, William L. Harrison, Ian Graves, Michela Becchi, and Gerard Allwein. Semantics driven hardware design, implementation, and verification with rewire. In Proceedings of the 16th Conference Languages, Compilers and Tools for Embedded Systems 2015 CD-ROM, LCTES'1K 15, New York, NY, USA, 2015. Association for Computing Machinery. ISBN 47814503325 doi: (0.1145/2670529.275//48 Published in Transactions Machine Learning Research (01/2025)
Pantuliano, Giambattista Parascandolo, Joel Parish, Emy Parparita, Alex Passos, Mikhail Pavlov, Andrew Peng, Adam Perelman, Filipe de Avila Belbute Peres, Michael Petrov, Henrique Ponde de Oliveira Pinto, Michael, Pokorny, Michelle Pokrass, Vitchyr H. Pong, Tolly Powell, Alethea Power, Boris Power, Elizabeth Prochl, Raul Puri, Alec Radford, Jack Rae, Aditya Ramesh, Cameron Raymond, Francis Real, Kendra Rimbach, Carl Ross, Bob Rotsted, Henri Roussez, Nick Ryder, Mario Saltarelli, Ted Sanders, Shibani Santurkar, Girish Sastry, Heather Schmidt, David Schnurr, John Schulman, Daniel Selsam, Kyla Sheppard, Toki Sherbakov, Jessica Shich, Sarah Shoker, Pranav Shyam, Szymon Sidor, Eric Sigler, Maddie Simens, Jordan Sitkin, Katarina Slama, Ian Sohl, Benjamin Sokolowsky, Yang Song, Natalie Staudacher, Felipe Petroski Such, Natalie Summers, Ilya Sutskever, Jie Tang, Nikolas Tezak, Madeleine B. Thompson, Phil Tillet, Amin Tootoonchian, Elizabeth Tseng, Preston Tuggle, Nick Turley, Jerry Tworek, Juan Felipe Cerón Uribe, Andrea Vallone, Arun Vijayvergiya, Chelsea Voss, Carroll Wainwright, Justin Jay Wang, Alvin Wang, Ben Wang, Jonathan Ward, Jason Wei, CJ Weinmann, Akila Welihinda, Peter Welinder, Jiayi Weng, Lilian Weng, Matt Wiethoff, Dave Willner, Clemens Winter, Samuel Wolrich, Hannah Wong, Lauren Workman, Sherwin Wu, Jeff Wu, Michael Wu, Kai Xiao, Tao Xu, Sarah Yoo, Kevin Yu, Qiming Yuan, Wojeiech Zaremba, Rowan Zellers, Chong Zhang, Marvin Zhang, Shengjia Zhao, Tianhao Zheng, Juntang Zhuang, William Zhuk, and Barret Zoph. Gpt-4 technical report, 2024.
Marcelo Orenes- Vera, Margaret Martonosi, and David Wentzlaff. Using Ilms to facilitate formal verification of rtl, 2023. URL https://axxiv.or//eae wttp://rrgg/abb//...oooo
Stanislas Polu and Iya Sutskever. Generative Language Modeling for Automated Theorem Proving. arXiv, September 2020. doi: 444550/arXiv.00000..
ACM SIGPLAN/SIGBER
URL
2754970
Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. Clover: Closed-loop verifiable code gener- ation. In ICLR 2024 Conference, 2024. URL http:p///pppaneeeeeeeereeerrrtrp
Gemini Team, Rohan Anil, Sebastian Borgeaud, Yonghui Wu, Jean-Baptiste Alayrac, Jiahui Yu, Radu Soricut, Johan Schalkwyk, Andrew M Dai, Anja Hauth, et al. Gemini: a family of highly capable multimodal models. arXiv preprint arXiv:2312. 11805, 2023.
Donald Thomas and Philip Moorby. The Verilog Hardware Description Language. Springer Publishing Company, Incorporated, 5th ed. edition, 2008 ISBN 0387849300.
Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannanch Hajishirzi, Yejin Choi, and Kyunghyun Cho. Naturalproofs: Mathematical theorem proving in natural language. In Thirty-fifth Conference on Newral Information Processing Systems Dalasels and Benchmarks Track (Round 1), 2021. URL
https://openrevier httt:://ppaarrreeeeeeee////tttas
Wikipedia contributors. N-gram Wikipedia, the free encyclopedia. https://en.wikis: org/
wiki/N-gran gramm 2024a. Accessod: 2024-03-27.
14

---

Published in Transactions Machine Learning Research (01/2025)
Wikipedia contributors.
Shellshock (software bug). Shellshock_ Shellshock_ (software_bug 2024b. Accessod: 2024-06-04.
htaps://on..ikkipctia..oo.//
Wikipedia contributors. Jaccard index wikipedia, the free encyclopedia, httpe://en.wikippeett
org/wilt//accard_inde 2024c. Accessed: 2024-03-27.
Kaiyu Yang and Jia Dong. Learning to prove theorems via intoracting with proof assistants, 2019.
Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models, 2023.
Lianmin Zheng, Liangsheng Yin, Zhiqiang Xie, Jeff Huang, Chuyue Sun, Cody Hao Yu, Shiyi Cao, Christos Kozyrakis, Ion Stoica, Joseph E. Gonzalez, Clark Barrett, and Ying Sheng, Efficiently programming large language models using sglang, 2023a.
Qinkai Zheng, Xiao Xia, Xu Zou, Yuxiao Dong, Shan Wang, Yufei Xue, Zihan Wang, Lei Shen, Andi Wang, Yang Li, Teng Su, Zhilin Yang, and Jie Tang. Codegeex: A pre-trained model for code generation with multilingual evaluations on humaneval-x, 2023b.
A Prompt Engineering for Annotation Reconstruction
of the previously largest such benchmarks, since they provide fairly rigorous procedent. We tried to keep prompts mostly the same across models in order to reduce the difference bet model performances that is caused by prompts. However, the prompts are not fully identical. For example, when we ask LLM to simply return the annotations-illlc program without any explanation, Claude 3 lends to add explanations that interfere with Dafny compilation. Thus, we had to adjust some prompts slightly to fit each model's peculiarities.
We based prompts the prompts used in the Clover benchmark (Sun et al. 2024
A.1 GPT Model Famly Prompts
SYSTEM_PROMPT
You are an expert in Dafny. You will be given tasks dealing with Dafny programs including precise annotations."
USER PROMPT 'Given Dafny program with function signature, preconditions,
postconditions, and code, but with annotations missing. Please return a complete Dafny program with the strongest possible annotations (loop invariants, assert statements, etc.) filled back in. Do not explain. Please use exactly the same function signature, preconditions, and postconditions. Do not ever modify the given lines. Below is the program:?' "
A.2 Claude 3 Opus Prompts
YYou are an expert in Dafny. You will be given tasks dealing with Dafny programs including precise annotations. You should only return code body in all circumstances. No text is alloved.
15

---

Published in Transactions Machine Learning Research (01/2025)
USER_PROMP?
' "Given a Dafny program with function signature, preconditions, postconditions, and code, but with annotations missing. Please return complete Dafny program with the strongest possible annotation (loop invariants, assert statements, etc.) filled back in. Do not explain or output any text. If you have to explain, put all explanations in comments form. There should only code body your output. Please use exactly the same function signature, preconditions, and postconditions. Do not ever modify the given lines. Below is the program: \n "err"daffn 'dafuyln'
A.3 CodeLlama-77-Instrucce Prompts
The prompts for
are the same those in A.2
B Proposals for Evaluating Strength of Generated Specifications
The evaluation of models' capability to generate formal specifications might be enhanced by integrat- ing the process with the creation of positive and negative test cases for each Dafny implementation. This approach proposes a reward system where models are evaluated based on the number of positive test cases their formal specifications support and the number of negative test cases they succossfully reject. However, this method introduces new challenge: ensuring the test cases accurately reflect the comprehensive meaning intended in the natural language descriptions. The consistency and validity of these test cases become critical, raising questions about the methods used to generate and verify them.
C Further Discussion
C.1 The Potential of Auto-Verifying Program Synthesis
Above discussed the challenge of verifying existing pre- vre-programs. Another potential of LLMs is to use wrogram-synthestt techniques that produce both programs and proofs of their correctness, all at the same time. This makes intuitive sense, since when a human programmer writes code, they typically have an informal proof in their head for why this code is correct. In other words, in addition to bridging the gap from low level implernentatio to high level specification in the upward direction, LLMs can offer assistance in generating provably correct low level code from high level specifications via program synthesis.
Current approaches to program synthesis enable engineers to encode a desired specification in high level language, and then through a (hopefully) verified correct compiler generate correct low level code in language like VHDL Committee & Subcommittee (2019) or Verilog Thomas & Moorby (2008) for hardware synthesis. Program synthosis limited by the need for a special purpose language or compiler to be constructed and verified correct its own right. For example, ReWire, a domain specific language defined as subset of Haskell Procter et al. (2015), was manually verified correct using the Coq Interactive Theorem Prover. In order to add new high-to-low path, new
16

---

Published in Transactions Machine Learning Research (01/2025)
language or compiler will need to be defined and verified. If an engineer needs synthesize correct Verilog rather than VHDI, they would likely need to first learn Caisson Li ct al. (2011).
LLMs offer way to generalize this approach. Starting with high level language, an engineer might be able to specify a system and then leverage a LLM to generate low level code with the corresponding loop invariants, weakest pre-conditions, strongest post-conditions, etc, included. Early results indicate that an LLM that is able to converse with a human when producing a program can reduce the error rate against simple programming benchmark by half Austin et al. (2021). If instead of receiving feedback from a human, the LLM were to interact with suite of formal verification tools, we expect further improvements. The LLM should be capable of generating code that is appropriately annotated for theorem proving, which is exactly the skill assessed by test benches like that described here.
D The Minhash Deduplication Algorithm
We can think about deduplicating a set of files by finding groups of "similar and then choosing only one file representative from each group to form our final deduplicated set of files. To do this, we can use the Jaccard similarity metric to decide whether one document is a duplicate of another.
The Jaccard similarity metric provides a way to quantify the similarity of two sets. It defined as Wikipedia contributors 2024ch:
JABB TAUB B
J(A, B)
In the application to code files, could consider each file to be set of n-grams, where an n-gram is defined a sequence of adjacent symbols in particular order (Wikipedia contributors 2024a and then apply the Jaccard score Jaccard score, we would need to run string comparison on every n-gram, which would have time complexity O (nm?) we have n n-grams each with max length m characters. This turns out to be an inefficient method for representing each code file as a set. Instead, the minhash deduplication algorithu approximates the Jaccard similarity between two documents by shingling the documents and comparing the minhash representation of each set of shingles (i.e. we compare fingerprints of documents instead of full documents). The minhash representation of a document is way to represent a text document with fixed set size that is smaller than the total number of n-grams in the document (i.e. the minhash representation of the document is a form of numerical fingerprint of the document). In Figure 7 below, we provide the pseudocode for the minhash algorithm used, based entirely on the script (Mou et al. 2023
similarity metric for our files. To directly calculate this
a set of numbers that is faithful to the structure of its content but
Note that the probability two files have the same min hash value under the same hash function equivalent to their Jaccard similarity. Concretely, for file A and file B:
[rii (a(A) = min h; J(A,B)
where min h20) denotes taking the minimum hash value under hash function h4. This makes sense because, assuming negligible hash collision, Pr hmin:;(A) min h;(B)) is equivalent to the
17

---

Published in Transactions Machine Learning Research (01/2025)
fuaction minhash, minhash_dedupl-e deduplicatiion (documents, aus_permutatione, threshold):
# Preprocess the documents
for each document in documents:
tokenize the document into n-grams (shingles)
hash each a-gram using hash function (e.g., xxHach SHA-1) store the hashed n-grams in set
Cenerate permutations for from pum.perautation:
generate randon coefficients and create permutation function: (a
prime_modulus
Create minhash signatures
signatures
for each document in documents:
signature -
for each permutation function:
min_hash INFINITY
for each hashed n n-gram in the document:
apply permutation function to hashed n-gram min_hash = min (min_hash, hermuted_hash)
perauted_hash
append min_bash to signature append signature to eignatures
Perform Locality-Sensitive Hashing (LSH)
achieve Jaccard similarity threshold of 0.5 really only need band (1.e. hash table)
250 permutations,
num_ sun_bands rows_per_band nun_permutations num_bands
number of bands
candidate_pairs
for each band:
create an empty hash table
for each document signature:
band_signature subset of signature for the current band hack_bucket
add document to the corresponding hash bucket for each hash bucket:
if number of documents in the bucket 1: generate all pairs of documents in the bucket add pairs candidate_paire
Use union-find datastructure track groups of duplicates duplicates UnionFind() for each band:
hashtable:
each hash bucket:
hash_buckes
if backk)) continue
else:
cluster_id min min (hashhbbuckett for x in hash bucket: duplicates, union(x, cluster_id)
Perform deduplication deduplicated, documents [] for each document in documents:
if duplicates find_rooo (document) = document: add document to
deduplicated_docunetts
18
Figure 7: Pseudocode for the minhash deduplication algorithm (continued).

---

Published in Transactions Machine Learning Research (01/2025)
probability that the first n-gram hash of under h4 equal the first regram hash of B under hy If h2 is good hash function, then it uniformly distributes the hash values of the original n-gram hashes over the range of h4 Let denote the number of n-grams with equivalent hashes; let denote the number of n-grams from A with smaller hash values than the hash value of corresponding n-gram from B; let b denote the reverse of the previous category. Then, Pr [min (x(A) min (B(
given the uniformity of h1. Note that a+b+c
AnB
J(A
AUB
Repositories of Scraped Dafny Code
We provide a full list of all repositories whose data we used the scraped portion of DafnyBench Tables 5 6 When reporting the license information, "Renamed so N/A" implics that the original repository we scraped December 2023 no longer exists under that name. Otherwise, the repositories have either Microsoft open-source licenses, MIT licenses, GNU General Public License v3.0 licenses, Creative Commons Zero v1.0 Universal, Apache 2.0 licenses, "Other" (which is secretly an MIT License in strange format, which has been checked manually). In light of this, we release our derivative DafnyBench repository under an Apache 2.0 license and GNU General Public License v3.0. We note explicitly here that all files from repositories with the Apache 2.0 license have been modified from their original form.
F Dafny Verification Examples
We take one example test program from DafnyBench, and consider four possible results for the corresponding LLM-reconstruutedd program: successfully verifies, fails to verify, cheats by including assume false, and cheats by including {:verify false). The last three cases are all considered fail by the Dafch evaluation metric.
F.1 Successful Example
Figure shows Dafny program that considered to have successfully verified without cheating.
Dafny verifier message: Dafny program verifier finished with 3 verified, 0 errors.
F.2 Failed Example
Figure 9 shows Dafny program that fails to be verified.
Dafny verifier message: (20,11): Error: index out of range. (30,4): Error: a postcondition could not be proved on this return path. (11,28): Related location: this is the postcondition that could not be proved. Dafny program verifier finished with 2 verified, 2 errors.
F.3 Cheat Example
Figure 10 shows that Dalny program cheats by including assume false, which Dafny Bench evaluation would count as fail.
Dafny verifier message: Dafny program verifier finished with 3 verified, 0 errors.
19

---

Published in Transactions Machine Learning Research (01/2025)
Table 4: Repositories from which Dafny Bench utilizes scraped code (no particular order).
Repository Name
License
dafi
No license provided
Grind-
No license provided
teup-mies
MIT License
Dainy
GNU General Public License v3.0
nitwit
MIT License
Dafny-experiences
No license provided
Formal Verification With Dafny
No license provided
SENG2011
No license provided
M2
No license provided
No license provided
t1
MF
No license provided
dafn--xeeccise
Other
dalny-learn
No license provided
sottwaresppecfication-1
No license provided
FMSS-2022-2022
The Unlicense
fv2020
No license provided
type-dctintion
No license provided
laboratory
No license provided
dafny
GNU General Public License v3.0
TFG
GNU General Public License v3.0
SiLemma
MIT License
dalny-training
No license provided
Methods
No license provided
dainy misc
MIT License
vmware- wwware-verifieee -erirare-erffcaaioo-22222
No license provided
CSU55004 Fornal-Veriliation
No license provided
MIEIC mies
MIT License
Dalny-programs
No license provided
MFES 2021
MIT License
DafnyPrgrrams
No license provided
CS357
No license provided
tormal www.aa/mmmmmmoi--ooooeeeeeeeenie
No license provided
Dainy ProgrammingLanguagee
No license provided
CSC8204-Dafny
No license provided
BPTree-veril
No license provided
tangent-finder
No license provided
Trabi-Metodos- Formais
No license provided
verified-usigg-dae
MIT License
Metodos Formais
No license provided
lets- blls-provebboociing-ueee
Creative Commons Zero v1.0 Universal
Datny Programs
No license provided
dainy workyw
MIT License
20

---

Published in Transactions Machine Learning Research (01/2025)
Table 5: Repositories from which DafnyBench utilizes scraped code (no particular order), continued.
Repository Name
License
Dafny-Prose Projotss
No license provided
Verieled Dafny
No license provided
dainy projects
No license provided
puers-metodos -ttt---metooo---omiiist-- formais-tl
No license provided
specTTesting
No license provided
QS BoilerPlatel
No license provided
datny-sandbox
No license provided
Formal- Verification
No license provided
datny-duck
No license provided
Flex Woek
No license provided
703FinalProjjp
No license provided
MFS
No license provided
dalny-mini-project
No license provided
Software- Veriffictinn
No license provided
Sireular-queu--imlleeeeee
No license provided
Final-Project-Dahhe
No license provided
DannyProjed
No license provided
bblny
No license provided
No license provided
No license provided
ssflysseeanalysis
No license provided
veriiiveiiiioationn
No license provided
datny-aoc-2019
No license provided
ProjectosCVS
No license provided
MFDS
MIT License
group heory
No license provided
Sadny-llnggaage-eevve
Other
Invoker
Apache License 2.0
formal-
Sormal-verfficatoon
No license provided
datny-programs
No license provided
ironsync-osdi21223
Other
verified-isort
No license provided
paxos proof
No license provided
sc2011
No license provided
Dainy Verify
No license provided
Formal-
Maeimal--ethhdd-PProee Project
No license provided
630-dainy
No license provided
dafny _xxmmless
MIT License
Workshop
No license provided
Dafny-Prea Practice
MIT License
CVS-handone
No license provided
C5404-tina--project
No license provided
21

---

Published in Transactions Machine Learning Research (01/2025)
Table 6: Repositories from which DafnyBench utilizes scraped code (no particular order), continued.
Repository Name
License
iron-syne
Other
stunning-palle palm-lree
Crealive Commons Zero v1.0 Universal
sat diy
No license provided
verilication-class
MIT License
AssertivePrograming
No license provided
Dafny-VMC
MIT License
libraries
Other
cmsc433
No license provided
Correctness
No license provided
CVS-Projtol
No license provided
dafleet
MIT License
datny-rope
MIT License
protoco--verfficaiion--2200
No license provided
vfag
No license provided
Dainy Learning Experience
Apache License 2.0
summer-school-2222
No license provided
BinaryScarch
Renamed so N/A
Iln-verilied-eval
MIT License
P
Renamed so N/A
Fun-Soluion
Renamed so N/A
C0
Renamed so N/A
Dainy Exercises
No license provided
dest-ganeration-exxmplsss
No license provided
HATTRA-2222PPaper
No license provided
veri-sparse
No license provided
Formal- Verification-Projer
No license provided
formal verication dainy
No license provided
Simulink-To dafny
No license provided
dafny experiments
No license provided
cs686
No license provided
P
ProgrammVeen
Trogran-Verifcatiion-aalldd Verifreation-Dalasel
MIT License
Dafny-demo
No license provided
dalny-exercises
No license provided
metodosFormais
No license provided
CS5232 Project
No license provided
Dafny-Exercises Exercises
No license provided
22

---

Published in Transactions Machine Learning Research (01/2025)
fuaction sorted array<int>) bool
reads
{
forall 1,1 int 1 0 <= x < Length = a[i] <= a[j]
}
method BinarySearch (a: array<int>> int) (index: int) requires sorted
ensures <= index Length [index]] == Length a[i] !=
index
=E> forall int
var los := 0;
var high := a. Length 1;
var mid : 0;
while (low high)
invariant <= lou <= high <= L.Leng invariant x lin a lou] & x !in alhigh 1..]
mid :- (high lou) / 2;
if [mid] < {
low mid + 1:
else if a[mid] high mid
else return nid;
return -1;
Figure 8: An example response that successfully fills annotations back in and verifies without cheating.
F.4 Another Cheat Example
Figure shows that another Dafuy program cheats by including (:verify false}, which Dafny- Bench evaluation would count as fail.
Dafny verifier message: Dafny program verifier finished with 3 verified, 0 errors.
G Overdetailed Specification
Figures 12 and 13 show two example programs update_array. serray_strong dfy and triple_sitteeeeee sii__strongddee dfy from the Clover benchmark (Sun al. 2024), in which the formal specification closely echoes the program implementation.
23

---

Published in Transactions Machine Learning Research (01/2025)
fuaction sorted <int>> bool
reads
{
forall 1,1 int <= < Length = a[i] <= a[j] 0=
}
method BinarySearch (a: array<int>> int) returns (index: int) requires sarted
ensures <= index Length [index] ==
index
=E> forall int Length a[i] !=
var los := 0;
var high := a. Length 1;
var mid : 0;
while (low high)
mid :- (high lou) / 2; if a[ii]] x {
low :- mid + 1;
else if a[mid] > x
high :- mid
else mid;
return -1;
}
Figure 9: An example response that fails to be verified, as it lacks necessary invariant statements.
H Ethics Statement
In creating DafnyBench, we took and reference every repository from which acquired this data, along with their licenses, in Appendix E. Furthermore, we cite the existing verifiable programming benchmarks that we subsume Dafny Bench (i.e. Clover Sun et al. (2024) and dafny-synthesis Misu et al. (2024)), and we asked explicit permission from their authors in order to do so. Finally, we cite all models that were used for evaluations on this benchmark OpenAT al. (2024): Brown al. (2020); Anthropic (2024); ; hug (2022). We used these models in accordance with the policies set forth in their API and model card documentation.
only data that publicly available GitHub,
Reproducibility Statement
Our benchmark contains the 782 ground_trutt programs and the corresponding verification ctt.icatiiooconationnssss sonddttioss_reoveedd removed programs. Additionally, we include full metadata on all of these files and the evaluation scripts necessary for running the listed models on them. By using the OpenAl and Anthropic APIs, others looking to reproduce this work should not expect to
24

---

Published in Transactions Machine Learning Research (01/2025)
fuaction sorted <int>> bool
reads
{
forall 1,1 int 0 0 <= ( < Length = a[i] <= a[j]
}
method BinarySearch (a: array<int>> int) (index: int) requires sorted
ensures <= index Length [index]] ==
index
==> forall int Length a[i] !=
assume false;
var los := 0;
var high :- a. Length 1;
var mid :- 0;
while (low high)
{
mid :- (high lou) / 2;
if a[id]] < x {
low i= mid + 1:
else if a[mid] x
high :- mid
else
mid;
return -1;
}
Figure 10: An example response that cheats by including assume false.
spend more than $300 for full run of GPT-4o on Dalch $300 for full run of Claude3 on DafnyBench, $500 for full run of GPT-4-turbo DafnyBench, and $400 for a full run of GPT-3.5 on Bench. We used the sglang package Zheng et al. (2023a) to efficiently query the models. All ovaluations were completed on a Linux cluster with an A100 Nvidia GPU.
25

---

Published in Transactions Machine Learning Research (01/2025)
function sorted <rray<int>) : bool
reads {
forall i, int O <= i < a.Lengh ".> a [4] <= a[j]
}
method fiverify false) BinarySoarch (a: array<int>, int) returns (index: int) requires sorted
ensures 0 <- index < Length [index] --
ensures index
.n> forall int < Lengnh .>> a[i] !-
low high Length 1;
mid :- 0;
while (low high)
mid : (high lou) / 2;
if [mid] < x {
low := mid + 1;
else if [mid] > x { high = mid 1;
}
else
return mid;
}
Figure 11: An example response that cheats by including {:verify false).
method OpdateElenents (a: array<int>) requires Length >=
modifies
ensures (1d()[4]) a[4]
ensures =[7]==516
forall
i<a. Length !- & a[i] old(a[i))
[4] a[4] 3:
[7] 516;
Figure 12: An example program update_ardt array_strongg dfy from the Clover benchmark (Sun al. 2024h, in which the formal specification closely echoes the program implementation.
26

---

Published in Transactions Machine Learning Research (01/2025)
method Triple (x:int) returns (r:int) ensures r==3*x
{
x+3;
Figure 13: Another example program triple_strong dfy from the Clover benchmark (Snn et al. 2024), in which the formal specification closely echoes the program implementation.
27


Reviews:
[{"review_id": "x45eXMgIUt", "reviewer": "Reviewer_CmfJ", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "**Strengths:**\n* Addresses a clear gap in formal verification benchmarks compared to mathematical theorem proving and program synthesis domains.\n* Comprehensive evaluation experiments on the proposed benchmark dataset with detailed analysis of different failure modes.\n* Thorough documentation of benchmark construction and evaluation procedures.\n\n\n**Weaknesses:**\n* It's clear that the new benchmark dataset is a better dataset for the evaluation with respect to this task as it has larger size and more difficult problems. However, since majority of DafnyBench problems are scraped from GitHub repositories, there's a significant risk of data contamination - the tested LLMs (Claude 3, GPT-4) may have already been trained on these Dafny problems. This is particularly concerning compared to other benchmarks such as Dafny-Synthesis. There's a higher chance that LLMs have memorized these problems which are directly in Dafny Language in Github compared to the ones that have been translated from MBPP Python problems to Dafny in the Dafny-Synthesis benchmark (Misu et al., 2024).\n\n* Beyond comparing dataset size and difficulty, it would be useful to see how LLMs perform across different data sources within DafnyBench (GitHub, Clover, Dafny-Synthesis). This could help to better analyze data contamination in LLMs' performance on GitHub-scraped problems versus the other benchmark sources.\n\n* Limited discussion of mitigation strategies for data contamination\n\n\nNOTE: Given that the paper's primary contribution is a benchmark dataset for evaluating LLM capabilities in formal software verification, I think that DMLR might be a better venue than TMLR.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "This paper introduces DafnyBench, a new larger evaluation benchmark for formal software verification, motivated by similar large-scale benchmarks in mathematical theorem proving and program synthesis. The benchmark contains over 750 Dafny programs, expanding upon existing verification benchmarks (Clover and Dafny-Synthesis) which had only 66 and 153 programs, respectively. \nThey evaluate modern LLMs like GPT-4 and Claude 3 on DafnyBench in generating correct annotations, showing that the best model achieves a 68% success rate.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "included in the weaknesses above.", "broader_impact_concerns": "None", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "Uyz6vqc1L3", "reviewer": "Reviewer_P2Bz", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strength: \n\n- The paper is well-written and easy to follow.\n- DafnyBench provides a broad collection of well-annotated Dafny programs, which can be a valuable resource for the formal verification community.\n\nWeaknesses:\n\nThe authors provide a fair assessment of the paper's limitations, particularly regarding the benchmark’s limited size, potential data contamination, and the lack of evaluation on translating natural language into formal specifications. Specifically:\n\n- The benchmark size (782 instances) remains very small. Expanding DafnyBench by manually constructing instances from other general programming benchmarks could further enhance its comprehensiveness.\n\n- The paper focuses on a single annotation-filling task. Introducing additional evaluation tasks, especially for generating formal specifications directly from natural language, would significantly enhance the benchmark's utility for Dafny and formal verification research.\n\n- The evaluation metric could be improved. Some annotations generated by LLMs may be simpler or more trivial than human-written ones, yet still technically correct. A more nuanced metric could better capture the quality and complexity of LLM-generated annotations.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "This paper presents DafnyBench, the largest benchmark designed for evaluating LLMs for formal software verification within Dafny. DafnyBench curates examples from open-source projects on GitHub, supplemented by two existing projects, to comprehensively assess the ability of various LLMs to generate Dafny annotations. Experimental results reveal that the most advanced LLMs achieve a success rate of approximately 68%. The study also highlights challenges in utilizing Dafny's feedback for model improvement and observes a significant performance decline with increasing program size or annotation complexity.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "- If feasible, consider extending the dataset size and incorporating additional evaluation tasks to broaden the benchmark’s applicability and rigor.\n- Add a manual evaluation of the generated annotations to verify whether the LLM-generated annotations align with the ground truth in both correctness and detail.\n- Table 2 reveals a significant disparity between the average and maximum values for various DafnyBench attributes. Displaying the distribution of these values would provide additional context and improve interoperability.\n- Figure 2 is referenced in the related work section (page 2) but appears on page 6, making it challenging to follow. Moving it closer to its initial reference would enhance readability.\n- Some statements require clarification. Many projects and benchmarks (particularly those using Coq and Isabelle theorem provers) focus on verifying software correctness (e.g., CompCert, SEL4), rather than purely mathematical theorem proving. Thus, statements like \"there are only 66 + 153 = 219 for proving program correctness\" are inaccurate and may overlook relevant related work.", "broader_impact_concerns": "N/A", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "vCl73doVhO", "reviewer": "Reviewer_d3dm", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "### Strengths\nThis paper is a solid paper overall, differentiating itself from prior work\nwhile also demonstrating appropriate continuity.  (This being said, I am not\nfamiliar with the literature at the intersection of formal verification and\nmachine learning, so I might be unaware of relevant work.)  The nature and\nstructure of the resources being introduced is clear, well-defined, and easy to\nfollow; that is, I feel like I have a good sense of what DafnyBench is having\nread the paper and how it could fill certain gaps in formal\nverification-focused program synthesis.  The data collection and filtering is\nwell-documented and appropriate for resource being created.  The task is\nclearly defined and is well-suited to the shape of the problem (e.g., using the\ncompiler to formally verify the program).  Finally the baseline methods and\naccompanying analyses give a brief but informative sense of how difficult the\nproposed task is and what next steps might be in improving performance on it.\n\n### Weaknesses\nI do not think there are any major weaknesses with the paper.  I believe the\nmost relevant weakness has to do with framing DafnyBench in terms of its\nintended uses, making it more difficult to determine the standard by which to\njudge the utility of the resource.  This is discussed more in the \"Requested\nChanges\" section.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "This paper introduces DafnyBench, a dataset of programs written in Dafny, a formal\nverification-focused programming language, along with an evaluation task which\nmeasures a system's ability to infer annotations necessary for the compiler to\nverify the given program.  The dataset comprises approximately 700 curated\nprograms collected from GitHub, a $6\\times$ increased compared to a comparable\nformal verification-focused dataset, yet far smaller than datasets on the\nrelated but distinct task of formal mathematical theorem proofs.  The\nevaluation metric that accompanies the dataset is a \"complete the program\" task\nwhere the model (usually an LLM) being evaluated must provide annotations to\na program (e.g., assertions, loop invariants) such that the Dafny compiler can\nverify the program constraints.  Finally, the paper tests the metric on\na handful of LLMs to give a sense of baseline performance on the task and what\ninsights the dataset and metric can produce.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "### Framing\nThe most important changes I would like to see in the paper are completing the\nframing which is already present.  This starts with giving a more robust sense\nof why the dataset is being introduced and how the proposed task/evaluation is\nimportant to formal verification as field.  While the introduction does a good\njob giving the context of formal verification generally, there is not as\nconcrete a sense given as to what DafnyBench will be used for.  Here are some\nparticular ways where answering this question is relevant:\n- How is program synthesis generally (i.e., no formal verification involved)\n  related or not related to what DafnyBench is addressing?  Clearly, there is\n  much more data for plain program synthesis, so going through all the trouble\n  of collecting Dafny data specifically should be justified by emphasizing the\n  contrast between what we might use the Dafny data for vis-à-vis the\n  limitations of what we can do with plain program synthesis data.\n- This exact same question is touched on but not robustly addressed with\n  respect to mathematical proofs: how are they the same? How are they\n  different?  I am not saying that I actually think there is no difference but\n  that by properly motivating and contrasting DafnyBench, it will help readers\n  understand if DafnyBench is relevant for their own research and how it might\n  be used down the road for research, say, unifying formal verification and\n  computer-verifiable mathematical proofs.\n- Is the evaluation task for DafnyBench only intended to be used with LLMs?  It\n  seems like the annotation task _could_ be performed by a simpler model, but\n  perhaps there are reasons for preferring the LLM (e.g., less task-specific\n  engineering).  Again, I think making it more clear why DafnyBench is being\n  introduced and what it will be used for will, in turn, make it clear why the\n  task is and ought to be LLM-focused.\n\n\n### Minor changes\n- (p. 2) \"Leino (2023)\" -> \"\\citep\"\n- (p. 3) The paper mentions that the way _dafny-synthesis_ was created could give a skewed distribution, but then later DafnyBench incorporates the data anyway; it seems a bit incongruous.\n- (p. 3) The description of how _Clover_ evaluates programs is a bit unclear.\n  I would recommend either going into less detail and not attempting to\n  describe its evaluation process or spend a little more time sketching it out,\n  because I was unsure of what _Clover_ was doing after reading the paragraph\n  (e.g., \"Why would it reject valid programs?\").\n- (p. 5) The introduction to 3.2 is a bit abrupt: are we now talking about the\n  task that DafnyBench uses to score the models?  A sentence or two introduce\n  this section would ameliorate this.\n- (p. 5) `\"cheat\"` $\\rightarrow$ ``` ``cheat''```\n- Sections 4.4 and 4.5 are a little sparse.  I think these sections should have\n  a bit more content---maybe a full paragraph.  The explication does not have\n  to be extensive, but there should be at least some indication of why these\n  observations are interesting/important.", "broader_impact_concerns": "Table 5 shows that a large proportion of the code included in DafnyBench is\nunlicensed.  While the strictest legal interpretations (at lest in places like\nthe United States) would suggest that one should not use unlicensed code, using\nsuch code (especially when it is published on an open source-centric platform\nlike GitHub) is standard operating procedure for machine learning research (for\nbetter or for worse).  That being said, I think it is important to note this\nfact in the main body of the paper.  Furthermore, it is also important to note\nif there is any material included that has licenses which notably differ from\nfree software license (e.g., non-commercial use licenses).", "additional_comments": "", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: The paper's main contribution is a new benchmark to test LLMs capabilities to annotate programs such that they can be formally verified (via the Dafny verifier in this case). Typically, providing such annotations is a tedious task for developers, as it means translating informal specifications into formal specifications - the potential speed-up through assistance and automation via LLMs is large. The paper adds a benchmark with over 750 programs, which improves over the largest previously published benchmarks by a large margin, and thus enables larger scale research. The paper also provides promising first results on the benchmark with GPT-4 and Claude 3 (under different prompting schemes), that show the potential for assistance and partial automation and also highlight the challenges for full automation with current state-ofthe-art models.

Overall, I think the paper makes an important contribution to drive forward and enable larger-scale research on automating formal verification with LLMs (verifiers exist, but the annotations are the bottleneck). While the size of the benchmark is still moderate, the authors put significant effort into collecting the dataset, which, together with the improvements in size compared to previously available benchmarks, is an non-trivial and significant contribution. The unavailability of licences for some of the examples (though all examples are publicly available) is a bit annoying, and may hinder adoption by commercial research labs, so if possible it would be great to try and rectify this in the future. Nonetheless, the work is clearly ready for publication and I have no open concerns or remaining issues from the reviewer discussion.
Decision: Accept (poster)