# Towards AI-Assisted Synthesis of Verified Dafny Methods

Md Rakib Hossain Misu  University of California IrvineIrvineCaliforniaUSA
<EMAIL_ADDRESS>0000-0002-7931-6782 ,  Cristina V. Lopes  University of
California IrvineIrvineCaliforniaUSA<EMAIL_ADDRESS>0000-0003-0551-3908 ,  Iris
Ma  University of California IrvineIrvineCaliforniaUSA<EMAIL_ADDRESS>0009-0003-3699-7981 and  James Noble  Independent ResearcherWellingtonNew
Zealand<EMAIL_ADDRESS>0000-0001-9036-5692

(2024; 2023-09-29; 2024-01-23)

###### Abstract.

Large stochastic language models show great promise in many domains, including
programming. A promise is easy to make but hard to keep, and language models
often fail to keep their promises when applied to programming, generating
erroneous code. One promising avenue to keep models honest is to have them
generate code in a language that supports formal verification: if and when
that is adopted, the model would provide proof along with the code, and that
proof would be automatically verified. Unfortunately, existing large language
models show a severe lack of proficiency in verified programming languages.

In this paper we demonstrate how to improve two pretrained models’ proficiency
in the Dafny verified programming language. Using 178 programming problems
from the MBPP dataset, we prompt two contemporary models (GPT-4 and PaLM-2 )
to generate methods in Dafny. We use three different types of prompts: a
direct contextless prompt, a second one that includes a signature of the
method and test cases, and a third one that decomposes the problem into steps
and includes dynamically chosen similar examples. Our results show that GPT-4
is better than PaLM-2 , but that, in both models, the third prompt greatly
improves the success of the generation task with respect to the direct prompt.
With the third prompt, GPT-4 was able to generate verified (and human-
evaluated) Dafny methods in 58% of the cases, while the first prompt generated
verified (and human-evaluated) methods in only 19% of the cases. Surprisingly,
the second prompt had the worst performance, with only 10%.

One tangible contribution of our work is a collection of 153 MBPP problems
that are implemented and formally verified in Dafny, 50 of which were written
by us and 103 were automatically synthesized by GPT-4 . Additionally, our
results demonstrate that the benefits of formal program verification (proof of
correctness) are now within reach of large stochastic language models used to
generate code. These results also demonstrate that program verification
systems can likewise benefit from incorporating large language models, whether
to synthesize code wholesale, to generate specifications, or to construct
internal verification annotations such as loop invariants, that are hard for
programmers and verification tools to find directly. (e.g. legal arguments,
transport signaling, structural engineering, etc.) where solutions must be
correct, and where that correctness needs to be verifiable by existing formal
tools, or explained to (and understood by) designers and end-users.

Program Synthesis, Dafny, LLM, Program Verification

††copyright: acmlicensed††doi: 10.1145/3643763††journalyear:
2024††submissionid: fse24main-p653-p††journal: PACMSE††journalvolume:
1††journalnumber: FSE††article: 37††publicationmonth: 7††ccs: Software and its
engineering Formal software verification

##  1\. Introduction

Formal verification is increasingly being adopted to support the development
of high-quality, provably correct software. High-stakes domains, such as
security-sensitive systems, cryptographic libraries, aerospace systems, and
embedded software in medical devices, look to formal verification for
correctness guarantees.

For instance, CompCert C (CompCert, 2023) is a formally verified C compiler
that won the ACM Software Systems award in 2021;
111https://awards.acm.org/software-system in a comprehensive study (Yang et
al., 2011), researchers found no bugs in the CompCert C compiler compared to
GCC (GCC, 2023) and LLVM (LLVM, 2023) toolchains. This study motivated Airbus
to adopt CompCert C to help ensure safety and enhance aircraft performance
(França et al., 2011). The seL4 project (Klein et al., 2009), awarded the ACM
Software System Award in 2022, resulted in a formally verified high-assurance,
high-performance operating system microkernel employed to protect an
autonomous helicopter against cyber-attacks (seL4 Project, 2023). In order to
secure communication, both Chrome and Android use formally verified
cryptographic code (Erbsen et al., 2020). Similarly, Mozilla incorporated its
verified cryptographic library for Firefox performance improvement (Jacobs and
2020, 2023).

Formal code verification consists of two parts that go hand-in-hand: formal
_specification_ of software properties, and automated, or semi-automated,
_verification_ of those properties. Over the past 50 years, verification has
had a couple of major breakthroughs, first with the development of interactive
theorem provers in the 1960s (Nederpelt et al., 1994), and then, at the turn
of the millennium, with the development of Satisfiability Modulo Theory (SMT)
solvers (Barrett et al., 2021). Unfortunately writing program properties and
proofs is still a creative, manual process that requires significant effort,
experience, and expertise. Formal specification languages are closer to
mathematics than to regular programming languages, and necessarily incorporate
subtle concepts based on classical or constructive logics. For example,
writing the proofs for the seL4 microkernel was an eleven person-year effort
of a group of experts (Murray et al., 2013).  Another example: the
verification code of the CompCert C compiler is more than three times the size
of the original compiler code itself; it took three person-years to write the
complete verification code, which is approximately two lines of code in a day
(Leroy, 2009). The fact that these systems have received important awards is a
testament to how exceptional these efforts are.

In the universe of languages and systems for formal code verification, Dafny
(Microsoft, 2023a) stands out as having made a significant effort towards
usability by programmers, rather than mathematicians. Dafny is a strongly
typed imperative programming language with functional and object-oriented
features that supports code verification via Hoare Logic (Hoare, 1969)
assertions, preconditions, postconditions, and invariants (_aka_ design by
contract). Although algorithmic code in Dafny is similar to many other
programming languages, writing the formal specifications and auxiliary
verification assertions is still difficult (Faria and Abreu, 2023; Noble et
al., 2022).

Over the past year, stochastic Large Language Models (LLMs) have been
revolutionizing both the software industry and research in software
engineering. LLM-assisted tools such as GitHub-Copilot (Copilot, 2023) and
Amazon CodeWhisper (CodeWhisperer, 2023) have been accelerating several tasks
of software development such as code generation, transformation,
summarization, documentation, code review, program repair and synthesis.
Although their performance is impressive for straightforward tasks in the most
popular programming languages, given more complex problems or less familiar
languages (such as Dafny), LLMs tend towards producing
”hallucinations”222Respectable software engineers would call hallucinations
”faults”, ”errors”, or ”bugs”. (McKenna et al., 2023; Galitsky, 2023; Salvagno
and Taccone, 2023; Azaria and Mitchell, 2023) — inventing control structures
or APIs that do not exist in the target programming language, borrowing
features from other languages, often generating code that fails to type-check
or even fails to parse.

This paper describes our initial investigations into combining LLMs and
program verification. Our main aim is to evaluate how well LLMs can synthesize
correct Dafny code, including the formal specifications and validation
conditions so that the code passes the Dafny verifier: as part of that effort,
we are also interested in how the additional logical rigor required by
verification enhances or degrades generation performance. This paper makes the
following contributions:

  * •

We conduct the first empirical study of LLMs synthesizing verifiable Dafny
methods.

  * •

We demonstrate that a prompt designed under the principles of Chain of Thought
(CoT) with semantically similar few shot examples explaining how to decompose
a problem step by step, can synthesize verified and correct Dafny methods with
meaningful specifications for 58% of problems in our test dataset.

  * •

We release the dataset MBPP-DFY-153, a collection of 153 programming problems
with specifications, solutions and tests in/for Dafny, based on the MBPP
(Mostly Basic Python Programming) dataset curated by Google (Austin et al.,
2021).

  * •

We demonstrate that program verification techniques can help ensure code
generated by LLMs is correct.

Our conclusions lead to a number of actionable insights. Most obviously, our
first contribution means that programmers developing Dafny systems could
already consider using LLMs — indeed, for simple cases, an LLM may be able to
generate both the specificiations of a Dafny method, and a verifiably correct
method implementation that meets those specifications. For researchers in LLMs
or verification, our second contribution, the dataset of 153 formally verified
Dafny examples, should enable further development of prompts and models to
improve the performance of LLMs.

Ultimately, synthesis of verified methods (let alone whole programs) is a huge
problem space consisting of multiple sub-problems: this paper is an initial
exploration of this space. Whereas our first two contributions speak to the
end to end task of synthesizing specifications and implementations from a
narrative prompt, our third contribution highlights that LLMs may prove more
effective at tackling sub-parts of the problem: generating just specifications
from narrative prompts, or code from specifications (with or without other
prompts), generating parts of method bodies, or generating only verification
annotations, such as loop invariants or termination conditions.

Taken together, these results lead to two intriguing speculative ideas: that
efforts on LLMs for code should concentrate on generating verifiable programs;
and that our approach of combining LLMs with program verification techniques
should transfer to other problem domains.

##  2\. Background & Motivation

###  2.1. Dafny: A Verification-Aware Programming Language

Dafny (Microsoft, 2023a; Leino, 2020) is a verification-aware statically typed
programming language which was first developed in Microsoft Research (MSR)
(Microsoft, 2023b); it is currently being developed with the support of the
Amazon Automated Reasoning research group (Amazon, 2023). Dafny includes
various features of several programming paradigms such as imperative,
functional, and object oriented programming. Its toolchain includes
translators for generating executable code in different target languages such
as C#, Java, JavaScript, Go and Python (Dafny, 2023). But the distinguishing
feature of Dafny is that it supports code verification via design by contract.
For that, it follows the framework of Floyd-Hoare-style (Hoare, 1969) program
verification with preconditions, postconditions, loop invariants and other
high-level formal proof synthesis features such as pure functions, predicates,
lemmas, and automated proof by inductions.

To develop a verified program, developers write Dafny code along with the
specifications (pre-and post-conditions), and then add loop invariants and
assertions that help the Dafny verifier prove the correctness of their code.
While coding in VS Code, the Dafny static program verifier checks the
functional correctness based on developers’ defined specifications and
annotations. Correctness means the absence of any runtime errors with respect
to the formal pre- and post-conditions, which means that the code does what
the developers specify it to do. In order to confirm that the developer

Find the smallest element in an array ⬇ 1 : method FindSmallest(s: array<int>)
returns (min: int) 2 : requires s.Length > 0 // preconditions 3 : //
postconditions 4 : ensures forall i :: 0 <= i < s.Length ==> min <= s[i] 5 :
ensures exists i :: 0 <= i < s.Length && min == s[i] 6 : { 7 : min := s[0]; 8
: for i := 1 to s.Length 9 : invariant 0 <= i <= s.Length //loop-invariants
10: invariant forall k :: 0 <= k < i ==> min <= s[k] 11: invariant exists k ::
0 <= k < i && min == s[k] 12: { 13: if s[i] < min { min := s[i]; } 14: } 15: }
16: //Main program, with a test case (checked statically!) 17: method Main() {
18: var a1:= new int[] [1,2,3]; 19: var out1:= FindSmallest(a1); 20: assert
out1 == 1; 21: } Figure 1. An example Dafny method; FindSmallest

specifications holds, the Dafny program verifier first transforms the code
into an intermediate verification representation (IVR) known as Boogie IVR (Le
Goues et al., 2011) language that expresses the verification conditions into
predicate calculus (Leino, 2017). Next, an SMT solver tries to prove the
verification conditions. In this phase, the Dafny verifier is backed by an
advanced SMT solver known as the Z3 theorem prover (de Moura and Bjørner,
2008). The validity of these verification conditions implies the correctness
of the code under consideration (Leino, 2017). However, sometimes the Z3
solver cannot automatically reach the required proof, even though such proof
exists. In such cases, the developer intervention is required to give more
context in the specifications by writing auxiliary verification conditions in
the form of assertions, functions, predicates, and lemmas.

In recent years, Dafny has had major successes: Microsoft used Dafny to
formally verify security libraries and kernels (Klein et al., 2009; Erbsen et
al., 2020), distributed systems (Hawblitzel et al., 2015), and concurrent
programs (Hawblitzel et al., 2014); Intel is developing its hardware
encryption library using Dafny (Yang et al., 2023); ConsenSys successfully
applied Dafny for their Ethereum Virtual Machine (EVM) verification (Cassez et
al., 2023); Amazon implemented the Amazon Web Service (AWS) authorization and
encryption logic in Dafny and deployed the Dafny-generated Java code into
production (Cook, 2018; Chakarov et al., 2022).

###  2.2. Motivating Example

To illustrate how a Dafny program is statically verified, Figure 1 shows a
simple procedure to find, and return, the smallest number in a given input
array. The method FindSmallest is formally specified not just by the types of
input and output parameters, but also with preconditions (with requires
clause) and postconditions (with ensures clause). The postconditions, in
particular, are the properties that we want to ensure are true for this method
– i.e. what it means for this method to be “correct.” The Z3 SMT solver is
usually not powerful enough to infer the postconditions from functional code
alone; as such, developers must give additional hints, or verifiable
conditions, along with the code in order to help the solver prove correctness
of the postconditions.

In this particular case, the code contains a loop that modifies state, so we
can provide loop invariants (with invariant clause) that must hold in every
iteration of the loop; those invariants

are then checked by the SMT solver and, if they hold, that helps proving the
postconditions of the method. The Main method represents the entry point: it
invokes the method FindSmallest for some test inputs and checks (with assert
clause) the outputs. Like other specification clauses, the assert statements
are also statically checked. In this example the verifier tries to prove the
assertion based on the postconditions of the FindSmallest method. All
specification clauses such as requires, ensures, invariants, and assert are
used statically – these clauses are not compiled into the executable and, as
such, do not cause any runtime overhead.

Writing the functional code in Dafny is similar to writing code in other
programming languages. However, researchers observed that writing the formal
specifications and auxiliary verification code in Dafny is still difficult
(Faria and Abreu, 2023). For instance, in Figure 1, the FindSmallest method
requires 6 lines of formal specifications to verify a simple 5 line of
algorithmic code. This example substantiates that the difficulty of writing
formal specifications exponentially increases with the difficulty of the
verifying program (Noble et al., 2022).

###  2.3. Large Language Models (LLMs)

Large Language Models (LLMs) are a class of deep neural networks pre-trained
in publicly available data to perform a variety of downstream tasks in natural
language processing (NLP). In the past year, LLMs have significantly impacted
a wide range of application domains including code related tasks such as code
generation, comprehension, summarization, and transformation.

The recent improvement of transformer based models (Radford et al., 2018) such
as GPT (Generative Pre-trained Transformer) advanced the usages of LLMs in
many coding related tasks compared to other pre-trained models (Chen et al.,
2023; OpenAI, 2023a). For instance, CodeX (Mark Chen et al., 2021) is a
descendant of the GPT-3 based model trained on massive publicly available code
repositories in GitHub, and is capable of performing coding related tasks in
various programming languages. Codex powers GitHub Copilot (Copilot, 2023), an
AI-pair programmer designed to assist software developers. OpenAI (OpenAI,
2023b) has now discontinued its Codex APIs, and suggested researchers adopt
the successors of GPT-3 (GPT-3.5 and GPT-4). Recently Google released PaLM-2
(Rohan Anil et al., 2023) a new successor of their earlier PaLM (Aakanksha
Chowdhery et al., 2022) model which is very capable of code generation and
reasoning tasks.

Although many research studies have been published on the use of LLMs in many
coding-related tasks, very few of them explore these models’ capability for
synthesis of formally verified programs (First et al., 2023). One of the
obstacles is that languages for formal code verification are not very popular.
Hence, the training data available for LLMs to learn these languages, and
their underlying concepts, pales when compared to the amount of training data
available for popular languages such as Python, Java, C++, etc. Nevertheless,
LLMs have been found to be capable of working as generic reasoning engines,
including having the capability to solve complex problems and prove theorems
(Li et al., 2023; Wu et al., 2022) that motivates us exploring how LLMs with
the combination of theirs reasoning, theorem proving, and coding abilities can
contribute to synthesizing verified Dafny code, along with formal
specifications and validation conditions.

###  2.4. Prompt Engineering

Prompt engineering is a relatively new term and concept that emerged in the
context of LLMs. It denotes the practice of iteratively crafting prompts for
improving the generative power and fitness of purpose of an LLM. First coined
by Gwern Branwen in 2020,333https://gwern.net/gpt-3 prompt engineering has
become a thriving subfield of research in LLMs (Bach et al., 2022; Dang et
al., 2022; Deckers et al., 2023; Hou et al., 2022; Jiang et al., 2022b; Liu
and Chilton, 2022).

LLMs are nominally intuitive to interact with: we give them a prompt, and they
reply with a related text or image. The resulting output of the model relates
to our prompt in plausible form. However, when using LLMs for specific
technical goals, the simplistic approach of asking for something informally
usually ends up in disappointing results.

Prompt engineering involves a systematic approach of creating prompts that
effectively convey the desired downstream task to the pre-trained LLMs
(Reynolds and McDonell, 2021; Beurer-Kellner et al., 2023). The crafting of
prompts plays a significant role in the performance of LLMs retrieved
contents. The prompt template should be structured in a manner that aligns
with both the targeted task and the selected LLMs. Prompting techniques can be
employed to train the LLMs explicitly through few-shot learning, incorporating
a limited number of examples, such as method signatures and test cases. In the
context of formally verified programs synthesis, the prompts need to be
tailored for the targeted programming language (in our case Dafny) with
unambiguous task descriptions (Bach et al., 2022; Dang et al., 2022).

##  3\. Study Design

This study aims to investigate the current capability and potentiality of LLMs
at synthesizing formally verified methods in Dafny. Specifically, we seek to
answer the following research questions.

  * •

RQ1 [Contextless Prompting]: How effective are LLMs at synthesizing formally
verified Dafny methods from simple natural language problem descriptions?

  * •

RQ2 [Signature Prompting]: How does additional context (signatures and tests)
affect the synthesis outcome of LLMs?

  * •

RQ3 [Dynamic Few-Shot Prompting]: Do prompts designed with Chain of Thought
(CoT) and semantically similar few-shot examples explaining problem
decomposition step by step improve the synthesis outcome of LLMs?

###  3.1. Test Dataset: MBPP-san-DFY

In order to conduct our study, we needed a collection of problems that has
natural language problem description corresponding formally verified Dafny
code. We searched Dafny code in GitHub that yielded only 188 repositories
having no natural language specifications of the available code. We would have
to recover the informal natural language specifications from the formal code
but by doing so we might inject errors by using words with a different
intention than the original developers, or inject our own biases.

Since we aim to synthesize Dafny code from natural language specifications ,
for this purpose, we adopted the Mostly Basic Programming Problems (MBPP)
benchmark published by Google Research in 2021 (Austin et al., 2021), which
was used in prior program synthesis and verification studies. MBPP consists of
a collection of close to 1,000 crowd-sourced algorithmic tasks with text
descriptions, function signatures, concise implementations in Python, and
three test cases to check their functional correctness. The tasks focus on
basic arithmetic, array and integer sequences, and string processing. The
textual descriptions of these tasks are concrete enough that a human should be
able to translate them into code without any additional clarifications.

Solutions to 427 MBPP tasks have been inspected manually, and published as a
subset called MBPP-sanitized (MBPP-san). We based our data on MBPP-san.
However, since our goal is to synthesize _Dafny_ , we chose to remove tasks
that relied on Python-specific data types or external libraries, such as
regex, math, heapq, etc. 444Dafny does not have a standard library, much less
external libraries. Note that any Dafny libraries would need to be formally-
verified a prior, or else the Dafny tasks would become much more complex than
their Python versions. We culled 82 tasks, leaving a dataset of 345 problems.

In order to keep our study’s costs under budget, we randomly selected 228
problems. Out of these 228 problems, we picked a random sample of 50 to act as
verified Dafny exemplars (see below Section 3.2) leaving us with 178 remaining
problems for testing. We manually translated each of those 178 problem
descriptions, signatures, and test cases into Dafny, but we did not translate
the solutions’ Python code, or attempt to write specifications. This resulted
in our main test dataset, MBPP-san-DFY: 178 instances of MBPP-san problems,
each one with a description, method signature, and three test cases translated
to suit Dafny.

The MBPP problem set, and Python solutions to the MBPP problems, are publicly
available and it seems likely they would have been incorporated into the LLMs’
training sets. However, there are no Dafny implementations of MBPP. Therefore,
we hypothesize that employing MBPP-san-DFY dataset would not create any data
leakage in our experiment.

###  3.2. Human Written Dataset: MBPP-DFY-50

To perform Dynamic Few-Shot prompting, we needed a relatively large and varied
collection of verified Dafny methods that could serve as examplars to be
included in prompts. A search for an existing suitable collection proved
fruitless. Our best alternative was to translate a subset of MBPP-san into
Dafny ourselves, but now also translating the Python solution for each
problems into Dafny, then coming up with specifications (method pre- and post-
conditions, loop invariants) for each example, and finally doing whatever
annotation, correction, or rewriting was needed until the Dafny verifier would
signal that the method was correct.

In this process, we experienced first-hand how hard it is to formally specify
postconditions and to provide loop invariants and hints so that correct code
can pass the Dafny verifier. It took approximately 220 hours for the first two
authors to create this dataset of 50 formally verified problems, even with the
Python solutions, full access to Dafny documentation, books, blog posts by
experts, and Stack Overflow.

###  3.3. LLM Selection

Program synthesis in Dafny requires knowledge of Dafny syntax, as well as
reasoning and theorem-proving abilities (Noble et al., 2022; First et al.,
2023). Therefore, we looked for LLMs that possess a combination of these
abilities. To determine which LLMs to use, we performed a pilot study using
our handwritten dataset MBPP-DFY-50. We started by looking at GPT-4 (OpenAI,
2023a) and GPT-3.5 (Mark Chen et al., 2021) from Open-AI (OpenAI, 2023b),
PaLM-2 (Rohan Anil et al., 2023) and PaLM (Aakanksha Chowdhery et al., 2022)
from Google, and CodeT5+ (Wang et al., 2021), CodeT5 (Wang et al., 2023) from
Salesforce and Code-Llama (Rozière et al., 2023) from Meta. All these LLMs
have been explored in prior code generation, program synthesis, and reasoning-
related studies. Our pilot study consisted of querying all these LLMs with the
problem description, asking them to solve each. We then analyzed their
responses to get a sense of their reasoning abilities, and the quality of
their approaches compared to our ground truth.  For these 50 problems, CodeT5,
CodeT5+, LLaMA, Code-LLaMA, and PaLM were not able to synthesize a single
syntactically correct Dafny method with specifications, as all of them
encountered compilation errors. Even in GPT-3.5, we got only 5/50
syntactically correct solutions. However, GPT-4 and PaLM-2 generate verified
Dafny methods in 16/50 and 7/50 problems respectively. Based on this, we
decided to narrow our investigation to GPT-4 and PaLM-2 only.

###  3.4. Prompt Design

Based on the background literature and our pilot study, we knew that our
experiment would depend on the prompts we offered to the LLMs. Therefore, we
experimented with three different prompts.

####  3.4.1. RQ1 [Contextless]

To answer RQ1 we designed a simple prompt that identifies the programming
language (Dafny), the problem description, and instructions for how to format
the code response. Our prompt design is inspired by Austin et al. (Austin et
al., 2021). This kind of prompt works well for popular languages like Python,
JavaScript, Java, C#, and C++.

Contextless Prompt You are an expert Dafny programmer, and here is your task:
Write a method in Dafny to find maximum run of
uppercase characters in the given string.
You must return the method in the following form:
```dafny //Dafny Code ```

Signature Prompt You are an expert Dafny programmer, and here is your task:
Write a method in Dafny to find maximum run of uppercase
characters in the given string.  Method Signature: method maxRunUppercase
(str: string ) returns (res: int ) Your code should satisfy these tests: var
out1:=maxRunUppercase( "GeMKSForGERksISBESt" ); assert out1==5; var
out2:=maxRunUppercase( "PrECIOusMOVemENTSYT" ); assert out2==6; var
out3:=maxRunUppercase( "GooGLEFluTTER" ); assert out3==4; You must return the
method in the following form: ```dafny //Dafny Code ```

Figure 2. An example of Contextless and Signature prompt

The Contextless prompt instructs the LLMs to synthesize a Dafny method in a
single step without providing any additional context. Figure 2 (top) shows an
example of Contextless prompt. Since writing functional code in Dafny is
similar to writing code in high-level programming languages, with Contextless
prompt our goal is to establish a baseline of the LLMs’ knowledge of Dafny.

####  3.4.2. RQ2 [Signature]

For RQ2, we extended the Contextless prompt with the desired method’s
signature and three test cases (see Figure 2 (bottom)). Code generation
experiments for non-verified code often include test cases and signatures
(implicitly or explicitly) (Austin et al., 2021; Mark Chen et al., 2021). We
hypothesized that with the method signature and test cases LLMs can infer the
pre- and post-conditions that would be beneficial to synthesize complex
problems.

####  3.4.3. RQ3 [Dynamic Few-Shot]

Work in LLMs has shown that Chain of Thought (CoT) reasoning to decompose a
problem into multi-intermediate steps can lead to drastically improved
reasoning, especially for code synthesis tasks (Madaan et al., 2022; Wei et
al., 2022; Reynolds and McDonell, 2021; Beurer-Kellner et al., 2023).

Used together with relevant examples in the prompt, aka few-shot prompting, it
becomes possible to “teach” LLMs things that had a weak presence in the
training data. Inspired by this, we designed a prompt following the principle
of Chain of Though (CoT) with semantically similar few-shot Dafny method
examples where each example explains its problem decomposition step by step
and how to derive the implementation in Dafny. The thought process and
reasoning steps of this prompt was informed by our own experience with Dafny.
When we write Dafny methods, we start by defining the method’s signature,
followed by thinking about the pre- and post-conditions that should hold for
that signature. Then we write the functional code, i.e. the algorithm that we
believe should result in those postconditions to hold, and finally we add the
proof, i.e. the necessary loop invariants and verification annotations that
lead the Dafny verifier to conclude that the algorithm is, indeed, correct.

However, for a given problem, this prompt will be effective when semantically
similar examples of the given problem are included in this prompt. Therefore,
we sought for a heuristic that can be employed to search best examples for a
given problem. While creating our MBPP-DFY-50 dataset, we observed that the
postconditions are the most valuable parts of Dafny method specifications. For
each problem we tackled, we searched through the problems we had already
solved, looking for similar postconditions. We then used those examples to
guide the proof of the new problem. We identified a pattern that problems
having similar method signature and post-conditions require the same type of
Dafny proofs and code to solve the problem. This pattern motivated us to
develop a prompt chaining pipeline for selecting few-shot Dafny code examples
that have similar method signatures and post-conditions for a given problem.
Figure 3 depicts the high-level overview of our developed pipeline for prompt
chaining.

Figure 3. A high-level overview of the prompt-chaining pipeline for Dynamic
Few-Shot Prompting.

To select semantically similar Dafny methods based on postconditions, we
employed prompt chaining in two phases. In the first phase, for a given
problem, we simply prompt the LLM to generate the method specifications such
as signature and postconditions. To teach LLM how to generate such
specifications, we provided three few-shots examples of problem description,
method signature and postcondition pairs from our MBPP-DFY-50 dataset. We
elected these examples based on the semantic similarity of the given problem
description. An example of such specification prompting is shown in Figure 4
(top).

Dynamic Few-Shot Prompting [Specification Prompt] TASK: Write a method in
Dafny to convert a given string to uppercase. Method Signature: method
ToUppercase(s: string ) returns (v: string )  Postconditions: \- The length of
the returning string must be the same as the length of the input string \- All
lowercase characters of the input string are uppercase in the output string \-
All other characters are unchanged
\------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
//Two more semantically similar few-shots example TASKS
\------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
TASK: Write a method in Dafny to find maximum run of uppercase characters in
the given string.

Dynamic Few-Shot Prompting [Chain of Thought (CoT) Prompt] SYSTEM: You are an
expert AI assistant that writes Dafny programs. You are very good at writing
verifiable correct code in terms of preconditions and postconditions of
methods, and at finding the appropriate loop invariants for the
pre/postconditions to hold.
\------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
TASK: Write a method in Dafny that matches a word containing ’z’. AI
ASSISTANT: Step 1: Determine the method’s signature. In this case: method
ContainsZ(s: string) returns (result: bool ) Step 2: Determine the
preconditions. In this case: \- There are no preconditions, the method will
work. Strings and sequences are always not null. Step 3: Determine the
postconditions. In this case: \- The result is true if the input string
contains the character ’z’ or ’Z’ \- The result is false if the input string
does not contain the character ’z’ or ’Z’ Step 4: Write the code, its formal
specification, and the verification annotations that help the solver prove the
postconditions. In this case: ⬇ ‘‘‘dafny method ContainsZ(s: string) returns
(result: bool) ensures result <==> (exists i :: 0 <= i < |s| && (s[i] == ’z’
|| s[i] == ’Z’)) { result := false; for i := 0 to |s| invariant 0 <= i <= |s|
invariant result <==> (exists k :: 0 <= k < i && (s[k] == ’z’ || s[k] == ’Z’))
{ if s[i] == ’z’ || s[i] == ’Z’ { result := true; break; } } } ‘‘‘
\------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
//Four more semantically similar few-shot example TASKS
\------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
TASK: Write a method in Dafny to find maximum run of uppercase characters in
the given string.  AI ASSISTANT:

Figure 4. An example of Specification Prompt (top) and CoT Prompt (bottom)

In the next phase, we search for semantically similar Dafny methods in our
MBPP-DFY-50 dataset, incorporating the LLM generated specification response.
To perform the semantic similarity, we utilized OpenAI Embedding API that
computes semantic similarity based on cosine distance. For the given
specification generated in the first phase, we selected top five Dafny methods
examples from our MBPP-DFY-50 dataset. We used 5 examples so that we can fit
the whole prompt in LLMs’ context length (i.g., token limits). With these few-
shot examples, we then prepared a CoT prompt that first instruct LLMs to
synthesize the specifications according the problem decomposition steps and
then synthesize a Dafny method that satisfies these specifications. Figure 4
(bottom) depicts an example of our designed CoT prompt.

###  3.5. Evaluation Metrics

We evaluate LLMs’ synthesized verified methods against the Dafny verifier. The
verifier reports whether Dafny code is (a) syntactically correct and (b)
verified. We report the synthesis performance using the pass@k metric (Kulal
et al., 2019; Mark Chen et al., 2021; OpenAI, 2023a; Wang et al., 2023). In
our study, we use verify@k metric (similar to pass@k), where k sample methods
are synthesized per problem; a problem is considered to be verified if any
attempt verifies.

Automated quantitative metrics are only a weak proxy for performance of LLMs
in this task. In one extreme, the synthesized Dafny code may not contain any
formal specifications whatsoever; in those cases, the verifier will report
verification success. Synthesized methods may contain only weak and
uninteresting formal specifications that are trivial to verify. The most
challenging part of this study is to check whether LLMs are able to generate
the “right” and “strong” formal specifications — in particular,
postconditions. In order to assess the semantic correctness of the generated
verification code, we manually reviewed all verified methods. We also manually
inspected all the generated methods that failed to verify, to identify what
types of errors prevented verification.

###  3.6. Temperature Tuning

The “temperature” is an important parameter of all LLMs that controls the
randomness of the decoding process (OpenAI, 2023a; Rohan Anil et al., 2023).
In doing experiments with LLMs, it is important to identify the best
temperature for each experiment. Therefore, before running our experiments in
the entire MBPP-san-DFY dataset, we first performed a temperature tuning
experiment. We chose a random sample of 50 problems from our test dataset
MBPP-san-DFY of 178 problems employing the sampling procedures with 90%
confidence interval and 10% margin of error. Next, for each type of prompt, we
executed these 50 problems in four different temperatures
$T\in\\{0.0,0.25,0.5,0.75\\}$ in both GPT-4 and PaLM-2 . We evaluated the
synthesized Dafny methods with our evaluation metrics verify@k where
$k\in\\{1,3,5\\}$. As shown in Figure 5 , we observed that in Contextless and
Signature prompt, GPT-4 shows best performance in T=0.75. However, in Dynamic
Few-Shot prompt, GPT-4 is most effective in T=0.5. PaLM-2 demonstrates better
performance with T=0.0 in Contextless prompt. And in Signature and Dynamic
Few-Shot Prompts PaLM-2 works good in T=0.5. Thus, we used those values for
GPT-4 and PaLM-2 , and their respective prompts.

Figure 5. Temperature tuning for GPT-4 and PaLM-2 on a sample of 50 problems
in four different temperatures $T\in\\{0.0,0.25,0.5,0.75\\}$ for three
different prompts. The values in vertical axis represents the verified program
synthesis rate in verify@k (k=5).

###  3.7. Experimental Setup

We developed scripts to execute different prompts on different temperatures
through Open-AI’s API for GPT-4 and Google’s API for PaLM-2. For verifying the
code, we employed the latest Dafny 4.0.0 version
555https://dafny.org/blog/2023/03/03/dafny-4-released/. In March 3, 2023, a
new major version, Dafny 4.0.0, has been released that broke backwards
compatibility. Both GPT-4 and PaLM-2 may not know anything about this latest
version. In our prompts and few-shot examples we did not specify which version
of Dafny should be used. We verified our MBPP-DFY-50 dataset in Dafny 4.0.0.
For executing the experiments and verifying synthesized Dafny methods, we used
a MacBook Pro (13-inch, 2020), having 2 GHz Quad-Core Intel® Core™ i5
processor, 16GB RAM, 512 GB SSD and running macOS Ventura 13.4.

##  4\. Results and Analysis

To evaluate LLM synthesis of Dafny methods, we queried all 178 problems in
three prompts with their tuned temperatures (described in Section 3.6).
However, we noticed that LLMs cannot generate any Danfy method snippets if
they misunderstood the problem or had insufficient knowledge to solve those
problems. In such cases, LLMs returned a textual explanation why it cannot
generate any Dafny method snippets: we filtered out those responses. We then
analyzed the verification results quantitatively and qualitatively.

###  4.1. Quantitative Analysis

In this section, we explain and compare our quantitative analysis across three
different prompts for GPT-4 and PaLM-2 .

####  4.1.1. Verification:

Table 1 summarizes the overall verification results for three prompts queried
with their tuned temperatures. For example, in Contextless prompting at k=5,
GPT-4 synthesized 104 verified methods out of 178 problems, achieving a
verification success rate 58.42%. We notice that the verification success rate
improves with the increasing number of attempts. For instance, in Contextless
for GPT-4 in k=1, the verification success rate is 32.58% whereas at k=3 and
k=5 it jumps to 53.37% and 58.42% respectively. PaLM-2 was unable to generate
a single verified method for Contextless prompting even with several attempts.
In Signature prompting, the verification success rate also improves with the
number of attempts. Here, GPT-4 generated 95 Dafny verified methods (53.37%),
which is slightly lower than Contextless prompting. PaLM-2 gets a boost at
k=5, synthesizing 12 (6.74%) verified methods. Both GPT-4 and PaLM-2 attain
the best performance in Dynamic Few-shot prompting. GPT-4 got 114 verified
methods (64.04%) in k=5 that surpass Contextless prompting’s performance.
PaLM-2 achieved significant improvement with a 29.21% verification success
which is around 4X performance boost compared to Signature prompting.

Table 1. Summary of verified Dafny method synthesis on 178 problems. For each prompt, LLMs responses were generated with their tuned temperature (T) in verify@k (where $k\in\\{1,3,5\\}$) Prompts | GPT-4 |  | PaLM-2
---|---|---|---
Contextless | Temperature | verify@k | Temperature | verify@k
T=0.75 | k=1 | 58/178 (32.58%) | T=0.00 | k=1 | 0/178 (0.00%)
k=3 | 92/178 (51.64%) | k=3 | 0/178 (0.00%)
k=5 |  104/178 (58.42%) | k=5 |  0/178 (0.00%)
Signature | Temperature | verify@k |  | Temperature | verify@k
T=0.75 | k=1 | 59/178 (33.14%) | T=0.50 | k=1 | 12/178 (6.74%)
k=3 | 88/178 (49.43%) | k=2 | 9/178 (5.05%)
k=5 |  95/178 (53.37%) | k=3 |  12/178 (6.74%)
Dynamic Few-Shot | Temperature | verify@k |  | Temperature | verify@k
T=0.50 | k=1 | 86/178 (48.31%) | T=0.50 | k=1 | 30/178 (16.85%)
k=3 | 105/178 (58.98%) | k=3 | 43/178 (24.15%)
k=5 |  114/178 (64.04%) | k=5 |  52/178 (29.21%)

####  4.1.2. Postconditions:

In a naive interpretation, these results could indicate that the complicated
third prompt is not worth it, at least for GPT-4 . However, that is far from
being the case. Verification success does not mean that the solution was
properly formulated. Postconditions, specifically, are essential in formally
specifying what methods are supposed to do. The absence of postconditions is a
strong sign that the solution is not usefully verifiable: methods with no
specifications trivially avoid being wrong.

Table 2. Summary of specifications synthesis result, in both verified and unverified methods. For each prompt, LLMs responses were generated with their tuned temperatures at verify@k (k=5). Prompts | GPT-4 |  | PaLM-2
---|---|---|---
Contextless | Specifications | Verified | Unverified | Verified | Unverified
has postconditions |  56/104 (53.84%) | 48/73 (65.75%) | N/A | 104/176 (59.09%)
has preconditions | 64/104 (61.53%) | 47/73 (64.38%) | N/A | 2/176 (1.13%)
has both | 41/104 (39.42%) | 32/73 (43.83%) | N/A | 2/176 (1.13%)
has invariants | 40/104 (38.46%) | 28/73 (38.35%) | N/A | 4/176 (2.27%)
Signature | Specifications | Verified | Unverified |  | Verified | Unverified
has postconditions |  30/95 (31.57%) | 22/80 (27.5%) | 1/12 (8.33%) | 62/162 (38.27%)
has preconditions | 46/95 (48.42%) | 31/80 (38.75%) | 1/12 (8.33%) | 61/162 (37.65%)
has both | 21/95 (22.10%) | 19/80 (23.75%) | 1/12 (8.33%) | 61/162 (37.65%)
has invariants | 38/95 (40.00%) | 19/80 (23.75%) | 0/12 (0.00%) | 6/162 (3.70%)
Dynamic Few-Shot | Specifications | Verified | Unverified |  | Verified | Unverified
has postconditions |  114/114 (100%) |  61/61 (100%) |  52/52 (100%) |  123/123 (100%)
has pre conditions | 74/114 (64.91%) | 42/61 (68.85%) | 35/52 (67.30%) | 99/123 (80.48%)
has both | 74/114 (64.91%) | 42/61 (68.85%) | 35/52 (67.30%) | 99/123 (80.48%)
has invariants | 57/114 (50.0%) | 57/61 (93.44%) | 13/52 (25.0%) | 90/123 (73.17%)

For both the verified and unverified methods, we looked into the formal
specification synthesis results. In Contextless prompting as shown in Table 2,
we noticed that, although, GPT-4 generated 104 verified methods, only 56 of
them contain postconditions. Since the remaining 48 verified methods have no
postconditions, indeed, they cannot be considered formally verified. Regarding
unverified methods, GPT-4 generates postconditions in 65.75% of them. Similar
to GPT-4 , PaLM-2 also shows better effectiveness (59.09%) in synthesizing
postconditions in unverified methods. However, since these methods are
unverified, it may happen that either these postconditions are wrong or the
syntactic or semantic implementation of these methods is incorrect to prove
the correct postconditions. In our qualitative analyses we manually examine
these methods and their specifications to identify the actual reasons (see
Section 4.2).

In Signature prompting, the presence of postconditions gets worse. Only 30 out
of 95 synthesis methods from GPT-4 have postconditions whereas for PaLM-2 only
1 method out of 12 contains postconditions. For unverified methods the
presence of postconditions drastically drops for both GPT-4 (31.57%) and
PaLM-2 (38.27%). It indicates that including additional contexts in the prompt
did not bring any substantial benefit.

However, in Dynamic Few-Shot prompting, the specification synthesis results
outstandingly improves for both GPT-4 and PaLM-2 . According to Table 2, 100%
of both verified and unverified methods have postconditions. The primary
reason for having postconditions in all synthesized methods is the few-shot
examples with the CoT process. We designed this prompt to dynamically select
five few-shot example methods based on their postconditions’ semantic
similarity, and each of these examples includes a CoT process describing how
to determine the post-conditions in natural instructions and then in Dafny
method in the implementation. The design of this prompt made the LLMs follow
the manner by which the examples were implemented.

####  4.1.3. Preconditions:

In a Dafny method, preconditions are only required when certain properties or
assumptions must be hold before invoking the method. Having preconditions is
not a mandatory formal specification that needs to be proved by the methods’
implementation.

In our experiment with Contextless prompting, we found that 61.53% of GPT-4
generated verified methods contain preconditions and 39.42% contain both pre-
and postconditions (Table 2). Like postconditinos, the presence of
preconditions drops in Signature prompting where only 48.42% of verified
methods contain preconditions and 22.10% have both pre-and postconditions.
Unfortunately, in Contextless and Signature prompting, PaLM-2 specification
synthesis performance is trivial. However, for both GPT-4 and PaLM-2 , Dynamic
Few-Shot prompting enhances the specification synthesis performance. As
demonstrated in Table 2, on average 64% of verified and unverified programs
for both GPT-4 and PaLM-2 contain pre-and postconditions. It substantiate that
the design of Dynamic Few-Shot prompt considerably strengthens LLMs
specification synthesis performance.

####  4.1.4. Invariants:

When a Dafny method has a loop, it should contain invariants that need to be
maintained in each iteration of the loop. As shown in Table 2, in Contextless
prompt, on an average 38% GPT-4 synthesis methods contain invariants. In
Signature prompting, the number increases slightly for verified methods,
however, the presence of invariants exceptionally enhances for Dynamic Few-
Shot prompting in GPT-4 synthesis methods. According to Table 2, 50% of
verified and 93.44% of unverified methods contain at least one loop invariant.
On the contrary, PaLM-2 struggles to synthesize loop invariants for both
verified and unverified methods in Contextless and Signature prompting. Only
the Dynamic Few-Shot prompting outstandingly improves its performance to have
loop invariants in 25% of verified and 73.17% for unverified methods
respectively.

###  4.2. Qualitative Analysis

This section describes our manual investigation. The first two authors
manually examined all prompt responses, assessing the quality of the formal
specifications, specifically the postconditions of the verified Dafny methods
– again, postconditions are the key element for a correct formal
_specification_. During this manual inspection, when we have any doubt about
the implementation or specifications, we looked into our ground-truth dataset,
MBPP-san, and discussed with each other. The two authors independently
performed this manual tagging and reached a high Inter-Rater Reliability (IRR)
(Hallgren, 2012)(93.91% Cohen Kappa (Viera et al., 2005)), which ended up with
consensus at the end. We summarize our qualitative analysis findings in Table
3. The complete analysis results are available in our companion repository 8,
including all prompts, LLMs’ responses, verification results, Dafny method
snippets with our manual tagging.

Table 3. Summary of qualitative analysis of specifications synthesis in verified methods. For each prompt, LLMs responses were generated with their tuned temperatures at verify@k (k=5). Specifications | Groups | GPT-4 |  | PaLM-2
---|---|---|---|---
Prompts | Prompts
Contextless | Signature |  | Dynamic
---
Few-Shot
Contextless | Signature |  | Dynamic
---
Few-Shot
Postconditios | Strong | 34/56 | 18/30 |  103/114 (90.35%) | N/A | 1/1 | 35/52
Weak | 15/56 | 9/30 | 3/114 | N/A | 0/1 | 3/52
Wrong | 7/56 | 3/30 | 8/114 | N/A | 0/1 | 14/52
Preconditions | Required | 19/41 | 10/21 | 36/74 (48.64%) |  | N/A | 0/1 | 6/35
Optional | 22/41 | 11/21 | 38/74 | N/A | 1/1 | 29/35
Invariants | Strong | 10/27 | 5/16 | 51/57 (89.47%) |  | N/A | N/A | 13/13
Weak/Wrong | 17/27 | 11/16 | 6/57 | N/A | N/A | 0/13

####  4.2.1. Postconditions:

The goal of a postcondition is to make sure that the implementation is correct
based on the proofs. Here the term ”correct” implies that the postcondition is
strong enough to precisely capture all possible output values. We tagged the
quality of postconditions into three groups, Strong, Weak and Wrong. In
Signature prompting, PaLM-2 got only one verified method and that has Strong
postconditions. With regard to, Dynamic Few-Shot prompt, we found that in 14
cases, PaLM-2 misunderstood problems’ description and generated wrong method
implementation for those problems. However, it got Strong postconditions in 35
methods and Weak postconditions in 3 methods only. Although GPT-4 got 56
verified programs in Contextless prompting, we encountered 15 of them have
Weak postconditions. Table 4.2.1 exhibits such an example of Weak
postconditions. On the other hand in Signature prompting 9 of verified methods
contain Weak postconditions which are very trivial specifications to verify
correct implementation.

In Dynamic Few-Shot, GPT-4 ’s specification synthesis result is impressive.
Only 3 of verified methods got Weak postconditions and in 8 cases it
misunderstood the problems’ description generated wrong methods. One
interesting example of such cases where GPT-4 misunderstood the problem
description and generated Wrong method is illustrated in Table 4.2.1.
Specifically in Dynamic Few-Shot, GPT-4 got 90.35%(103/114) of verified
methods containing Strong postconditions.

Table 4. Examples of LLMs synthesis Strong, Weak and Wrong postconditions;
Required and Optional preconditions; invariants subsuming postconditions, and
modularization of proofs.

Specifications | LLM Synthesis Specifications in Dafny
---|---
Post- conditions | Strong |

Weak

⬇

/*Write a method in Dafny to interleave 3 sequence of the same

length into a single flat sequence.*/

method SplitAndAppend(l: seq<int>, n: int) returns (r: seq<int>)

requires n >= 0 && n < |l|

ensures |r| == |l|

ensures forall i :: 0 <= i < |l| ==> r[i] == l[(i + n) % |l|]

Wrong

⬇

//Write a method in Dafny to find the median of two sorted lists of same size.

method FindMedian(a: array<int>, b: array<int>) returns (median: int)

//...MISUNDERSTANDING

ensures median == if (a.Length % 2 == 0)

then (a[a.Length / 2 - 1] + b[0]) / 2 else a[a.Length / 2]

Pre- conditions Required

⬇

//Write a method in Dafny to compute the n-th power of each number in a list.

function Power(base: int, exponent: int): int //.. PROOF MODULARIZATION

requires exponent >= 0

{ if exponent == 0 then 1 else base * Power(base, exponent-1) }

method PowerOfListElements(l: seq<int>, n: int) returns (result: seq<int>)

requires n >= 0

ensures |result| == |l|

ensures forall i :: 0 <= i < |l| ==> result[i] == Power(l[i], n)

Optional

⬇

//Write a method in Dafny to append the given array to the given sequence.

method AppendArrayToSeq(s: seq<int>, a: array<int>) returns (r: seq<int>)

requires a != null

/*In Dafny arrays and sequences are never null,

unless the method declares them as array? and seq?*/

Invariants Subsume Post- conditions

⬇

/* Write a method in Dafny to check whether a list of sequence contains

the given sequence or not.*/

method ContainsSequence(list: seq<seq<int>>, sub: seq<int>) returns (result:
bool)

ensures result <==> (exists i :: 0 <= i < |list| && sub == list[i])

{

result := false;

for i := 0 to |list|

invariant 0 <= i <= |list|

invariant result <==> (exists k :: 0 <= k < i && sub == list[k])

####  4.2.2. Preconditions:

A precondition is an annotation that must be true before a Dafny method is
invoked. When a method is called, it is caller’s responsibility to make sure
that the preconditions are satisfied. The caller of the method then gets to
assume that the postconditions hold after the method returns (Dafny, 2023). To
keep in mind that, in our analysis, we did not call LLMs synthesis methods. In
our manual investigation, we only tagged preconditions into two groups, (i)
Required, which is necessary to prove the postconditions and implementation;
(ii) Optional, its presence is not required for verification. Table 3
demonstrates the summary of our preconditions analysis. Examples of LLMs
synthesis Required and Optional precondtions are illustrated in Table 4.2.1.

####  4.2.3. Invariants:

We reviewed loop invariants in all verified methods that have postconditions.
To determine loop invariants in Dafny, a common trick is to work backwards
from the postconditions and identify the loop guard (Dafny, 2023). While
examining responses, we recognized the same patterns followed by the LLMs. We
observed that GPT-4 and PaLM-2 both determined loop invariants mostly based on
the postconditions and in most of the problems loops invariants subsume some
or whole part of the method’s postconditions as shown in Table 4.2.1. We found
that all synthesis methods in three different prompts containing Strong
postconditions, also have correct loop invariants. And when the postconditions
were Weak or Wrong, loop invariants were intuitively incorrect for those
methods. In many cases we also noticed that GPT-4 guaranteed loop termination
(i.e, total correctness) with the explicit usages of decreases statement on
loop guards.

####  4.2.4. Modularization of Logic:

Dafny, supports predicate and function to write modularized and readable
auxiliary proofs code (Dafny, 2023). To keep in mind that, code written inside
predicate and function would not be compiled for runtime execution. When we
reviewed all verified synthesis methods, we encountered that only in Dynamic
Few-Shot prompting, many synthesis methods contain predicate and/or function
to modularize its proofs. We found that only 4 out of 52 PaLM-2 synthesized
verified methods have modularized proofs whereas for GPT-4 , 20 out of 103
verified methods have the usages of predicate or function. Table 4.2.1 shows
an example of such modularized proofs with the usages of function.

###  4.3. Error Analysis

Table 5. Summary of different types of errors found in unverified methods. For each prompt, LLMs responses were generated with their tuned temperatures at verify@k (k=5). Error Types | Error Name | GPT-4 |  | PaLM-2
---|---|---|---|---
Prompts | Prompts
Contextless | Signature |  | Dynamic
---
Few-Shot
Contextless | Signature |  | Dynamic
---
Few-Shot
Compilation Errors | parse errors | 51/73 | 44/80 | 16/61 | 176/176 | 152/162 | 43/124
resolution/type errors | 14/73 | 30/80 | 15/61 | 0/176 | 10/162 | 66/124
Verification Errors | loop invariant violation | 4/73 | 1/80 | 23/61 |  | 0/176 | 0/162 | 10/124
postcondition might not hold | 3/73 | 1/80 | 13/61 | 0/176 | 0/162 | 7/124
bound errors | 0/73 | 1/80 | 2/61 | 0/176 | 0/162 | 5/124
index out of range | 2/73 | 2/80 | 5/61 | 0/176 | 0/162 | 2/124
possible division by zero | 0/73 | 0/80 | 0/61 | 0/176 | 0/162 | 1/124
verification time out | 1/73 | 0/80 | 0/61 | 0/176 | 0/162 | 0/124

We manually analyzed the error logs for all unverified methods and identified
two major types of errors. We then examined the error types and classified
them into several subgroups. Table 5 demonstrates the presence of different
types of errors appeared in all unverified methods.

####  4.3.1. Compilation Errors:

We found compilation errors when a Dafny method was not verified because of
incorrect Dafny syntax or unknown types. These errors appeared in two forms
(i) parse errors, having wrong Dafny syntax and (ii) resolution/type errors,
when a method implementation contains usages of any unknown types. In our
manual inspection, we observed that the majority of LLMs synthesis methods
were not verified because of compilation errors. As shown in Table 5, in
Contextless and Signature prompting, 100% and 93.83% of PaLM-2 synthesis
methods were unverified because of parse errors. In Dynamic Few-Shot
prompting, parse errors were minimized, nevertheless, resolution/type errors
appeared in around 53.22% of cases. We inspected the reasons for
resolution/type errors and found that PaLM-2 generated Dafny methods assuming
the presence of basic library methods/functions without providing any
implementation. Consequently, the verifier raised a resolution/type errors
because of the usages of unknown method/function. Similarly, GPT-4 also
struggled generating correct Dafny syntax in Cotextless and Signature
prompting. In Cotextless, 51 out of 73 unverified methods have parse errors.
It gradually overcome and improved its performance in Dynamic Few-Shot
prompting where only 16 out of 61 unverified methods got parse errors.
Regarding, resolution/type errors, GPT-4 got such errors most (30/80) in
Signature prompting whereas in Dynamic Few-Shot prompting, GPT-4 got only 15
of such errors out of 61.

####  4.3.2. Verification Errors:

These types of errors occurred when a Dafny method has correct syntax,
however, the specifications or implementation were incorrect. We found six
different types of verification errors as exhibited in Table 5. Most of the
syntactically correct methods were unverified because of having loop invariant
violation and/or postcondition might not hold errors. In Contextless and
Signature prompting, we barely identified verification errors since most of
them got compilation errors. However, in Dynamic Few-Shot prompting, GPT-4 got
loop invariant violation errors in 23 cases and postcondition might not hold
errors in cases 13 out of 61 unverified methods. We observed that these errors
appeared because of two reasons (i) the specifications (postcondtions or
invariant) were correct but the implementation was incorrect to prove the
specifications and (ii) sometimes the implementation was right but the
specifications synthesis was incorrect.

###  4.4. Summary of Findings

RQ1 [Contextless Prompting]: Our experiments show that, with simple problem
description, LLMs can generate but not necessarily syntactically correct,
Dafny methods. Specifically, GPT-4 is capable of generating plausible Dafny
methods but it has serious difficulties generating the formal specifications.
Without proper formal specifications, the internal verification annotations,
when they exist, become moot.

RQ2 [Signature Prompting]: Unlike program synthesis in popular languages,
additional contexts such as method signatures and test cases seem to confuse
LLMs, and distracted the models away from formal specification generation and
verification. That is, the models paid more attention to testing than to
formal verification.

RQ3 [Dynamic Few-Shot Prompting]: Our results show that prompt designed
following the principles of Chain of Thought (CoT) with semantically similar
few-shot examples explaining problem decomposition step by step help LLMs
synthesize correct Dafny methods. In our experiment, this prompt design led
LLMs to generate formal specifications in 100% of the cases. Specifically for
GPT-4 , 58% of the generated Dafny methods are verified and contain meaningful
formal specifications.

##  5\. Related Work

###  5.1. Program Synthesis and Verification with Dafny

In the last 20 years, formal methods for software synthesis (Gulwani et al.,
2017) and verification (Ringer et al., 2019) have moved from an esoteric
research topic (Leino and Nelson, 1998) to a set of increasingly practical
tools, and from doctoral study to undergraduate degrees (Jones and Misra,
2021). Tools such as Dafny, SAW, and SPIN are increasingly mature enough to
support industrial application (Greengard, 2021; Wayne, 2018): indeed a main
barrier to adoption remains a lack of software engineers trained in their use
(Garavel et al., 2020).

Dafny is used in production to develop verified implementations of encryption
algorithms (Yang et al., 2023), of Ethereum Virtual Machine (EVM) bytecodes
(Cassez et al., 2023), and even of quantum circuitry (Li et al., 2022b). Dafny
is also the topic of ongoing research in verification and synthesis. Ahmed et
al. introduced XDsmith, a fuzzing differential testing framework that
generates random Dafny programs with known verification output (Irfan et al.,
2022). XDsmith evaluates the Dafny verifier’s soundness and precision and
conducts differential testing on the Dafny compiler to build robust programs.
In the Amazon Automated Reasoning group, Aleksandar et al. developed an
approach to generate counterexamples in Dafny syntax when the Dafny verifier
cannot establish a valid proof (Chakarov et al., 2022).

This work testifies to the ongoing relevance of Dafny-style program
verification in research, and increasingly in practice. Our results indicate
that LLMs are likely to be a fruitful direction for assisting with Dafny
programming, in both research and practice.

###  5.2. LLMs for Formal Methods

Researchers have been actively working on developing automated proof synthesis
and theorem provers (Sanchez-Stern et al., 2020). Several efficient proof
synthesis tools have been developed based on precomputed facts reasoning,
heuristic search and identifiers such as CoqHammer (Czajka and Kaliszyk,
2018), TacTok (First et al., 2020), Passport (Sanchez-Stern et al., 2023).
However, recently developed LLMs based approaches, for instance, ASTactic
(Yang and Deng, 2019), Diva (First and Brun, 2022) Thor (Jiang et al., 2022a)
and Baldur (First et al., 2023) outperforms these existing tool to synthesis
whole or partial proofs and automatically prove theorems employing interactive
proof assistants Coq and Isabelle/HOL.

Apart from proof synthesis and theorem proving, LLMs have also been applied to
translate natural language into formal specifications, proofs and mathematical
theorems (Qiao et al., 2023; Meadows and Freitas, 2022; Li et al., 2023).
Yuhuai et al. have translated natural language problems into Isabelle/HOL (Wu
et al., 2022), while Cunningham et al. experimented generating mathematical
proofs for code verification (Cunningham et al., 2022). To enhance reasoning,
Aman et al. generated event graphs (Madaan et al., 2022) and found that LLMs
trained on source code outperformed those trained only on text.

Most contemporary LLMs have limitations when it comes to algorithmic reasoning
(Austin et al., 2021) although this may be mitigated by careful prompting
(Zhou et al., 2022). While mighty ChatGPT can generate plausible texts about
mathematical problems, it cannot currently deliver correct mathematical proofs
or solutions (Frieder et al., 2023). The Minerva model, however, is pre-
trained on a mathematics corpus (First et al., 2023), and also aims to
generate proofs in Isabelle/HOL.

Stochastic learning techniques are in vogue in software engineering research
(Watson et al., 2022; Yang et al., 2022; Allamanis et al., 2018). LLMs have
been evaluated across a range of tasks such as code generation, code
completion, code summarization (Tufano et al., 2023; Nashid et al., 2023),
code repair (Yasunaga and Liang, 2020; Sintaha et al., 2023; Mashhadi and
Hemmati, 2021), program transformation and synthesis (Austin et al., 2021),
test generation (Mastropaolo et al., 2023; Tufano et al., 2022a), bug fixing
(Chakraborty and Ray, 2021; Tufano et al., 2019) code review (Tufano et al.,
2022b; Li et al., 2022a) — for some tasks, performing as well as or better
than the state of the art (Watson et al., 2022; Yang et al., 2022; Allamanis
et al., 2018), especially when prompts are carefully constructed (Nashid et
al., 2023). Recent studies suggest that applying LLMs to code-related tasks
has the potential to improve developer productivity (Nashid et al., 2023;
Chakraborty and Ray, 2021; Tufano et al., 2019).

All this work (both formal methods and programming tasks) focuses on careful
training of LLMs in mathematics — or otherwise extending their reasoning
power. Our results explore an alternative approach: letting LLMs do what they
are good at — generating plausible solutions — and then employing program
verification techniques to do what they are good at — verifying whether or not
those solutions are correct.

##  6\. Threats to Validity

Following the Siegmunds and Apel (Siegmund et al., 2015) and Feldt and
Magazinius (Feldt and Magazinius, 2010) we have considered a number of threats
to the validity of this study. For all research questions, the closed nature
of our experiments and the straightforward decision criteria (can Dafny
compile a program? verify a program?) should ensure construct and internal
validity: we are interested in the mechanistic question of whether a
contemporary language model can generate code for a verifiable programming
language, and we test that directly. Investigators’ subjective judgments are
engaged primarily to classify mistakes and assess the fitness of the
postconditions given the natural language prompts. We used standard human
evaluation method with consensus at the end. Any doubts about our judgments
are mitigated by the availability of all our data and judgements.

A threat to external validity is how well these results generalize to another
language model or other programming languages — or even to different versions
of the tools we evaluated. In designing the study, we were aware that both the
language model (GPT-4) and the programming language (Dafny) were evolving very
rapidly: the version of GPT-4 we used had been available for only 14 days and
Dafny 4.0 has been released on 3rd March 2023, and furthermore that those
versions of these tools embodied significant improvements over the earlier
versions. .

Thus the only sure assertions we can make about the detailed results of this
study are that they are unlikely to generalize: we expect the results will be
different — most likely, better — if we repeat the study with subsequent
versions of either the language model or the programming language.
Unfortunately, there is no way to avoid these problems when studying
contemporary versions of software under continual, rapid, development: but we
consider the advantages of using the latest versions outweighs any increase in
reproducability we could get by e.g. using the previous stable versions that
several years old. We have, however, mitigated this threat as well as
possible. We have identified the precise versions of the software and hardware
that we used. The research artifacts of this study are publicly available at
the companion GitHub repository.

##  7\. Conclusion

We investigated the potential of large stochastic language models (GPT-4 and
PaLM-2 ) to synthesize method specifications and code bodies in the Dafny
verification-aware programming language. We found that, given appropriate
prompts, GPT-4 can generate plausible imperative method bodies, the pre- and
post-conditions needed to specify those bodies, and the internal assertions
and invariants required for Dafny to verify the method bodies against the
method specification — in spite of the model’s vague understanding of Dafny
and its initial struggle with generating verifiable code. Instead of regular
prompting, a well-crafted Chain of Thought (CoT) prompt with semantically
similar few-shot examples explaining problem decomposition step by step
yielded the best performance, generating the most post-conditions and
minimizing unnecessary preconditions. Of the 178 problem in our test dataset,
58% of synthesized Dany methods were verified with meaningful specification
and many of the remaining cases involving minor errors. These findings
underscore the importance of careful prompt design and suggest that with
further improvement in prompt design and examples, GPT-4 can serve as an AI-
Assistant for writing formally verified methods in Dafny.

Finally, this work is an exploratory study. The results already demonstrate
great potential for further, more focused research on program synthesis.
Furthermore, we hypothesize that incorporating tools and techniques from
program verification may be a fruitful direction for research into generative
stochastic models more generally, whenever their output must not only be
plausible but also correct.

##  8\. Data Availability

The complete artifacts of this study, including the evaluation benchmark,
collection of verified Dafny code, prompts for each problem, LLMs’ response
and our manual evaluation all are publicly available in this GitHub
repository.  Dafny-Synthesis: https://github.com/Mondego/dafny-synthesis

## References

  * (1)
  * Aakanksha Chowdhery et al. (2022) Aakanksha Chowdhery et al. 2022.  PaLM: Scaling Language Modeling with Pathways.  _CoRR_ abs/2204.02311 (2022).
  * Allamanis et al. (2018) Miltiadis Allamanis, Earl T. Barr, Premkumar T. Devanbu, and Charles Sutton. 2018.  A Survey of Machine Learning for Big Code and Naturalness.  _ACM Comput. Surv._ 51, 4 (2018), 81:1–81:37.  https://doi.org/10.1145/3212695
  * Amazon (2023) Amazon. 2023.  Automated reasoning.  https://www.amazon.science/research-areas/automated-reasoning.  [Online], [Accessed: 2023-09-20].
  * Austin et al. (2021) Jacob Austin, Augustus Odena, Maxwell I. Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie J. Cai, Michael Terry, Quoc V. Le, and Charles Sutton. 2021.  Program Synthesis with Large Language Models.  _CoRR_ (2021).  https://arxiv.org/abs/2108.07732
  * Azaria and Mitchell (2023) Amos Azaria and Tom Mitchell. 2023.  The Internal State of an LLM Knows When It’s Lying. In _Findings of the Association for Computational Linguistics: EMNLP 2023_ , Houda Bouamor, Juan Pino, and Kalika Bali (Eds.). Association for Computational Linguistics, Singapore, 967–976.  https://doi.org/10.18653/v1/2023.findings-emnlp.68
  * Bach et al. (2022) Stephen Bach, Victor Sanh, Zheng Xin Yong, Albert Webson, Colin Raffel, Nihal V. Nayak, Abheesht Sharma, Taewoon Kim, M Saiful Bari, Thibault Fevry, Zaid Alyafeai, Manan Dey, Andrea Santilli, Zhiqing Sun, Srulik Ben-david, Canwen Xu, Gunjan Chhablani, Han Wang, Jason Fries, Maged Al-shaibani, Shanya Sharma, Urmish Thakker, Khalid Almubarak, Xiangru Tang, Dragomir Radev, Mike Tian-jian Jiang, and Alexander Rush. 2022.  PromptSource: An Integrated Development Environment and Repository for Natural Language Prompts. In _Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics: System Demonstrations_ , Valerio Basile, Zornitsa Kozareva, and Sanja Stajner (Eds.). Association for Computational Linguistics, Dublin, Ireland, 93–104.  https://doi.org/10.18653/v1/2022.acl-demo.9
  * Barrett et al. (2021) Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. 2021.  Satisfiability Modulo Theories.  In _Handbook of Satisfiability - Second Edition_ , Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications, Vol. 336. IOS Press, 1267–1329.  https://doi.org/10.3233/FAIA201017
  * Beurer-Kellner et al. (2023) Luca Beurer-Kellner, Marc Fischer, and Martin Vechev. 2023.  Prompting Is Programming: A Query Language for Large Language Models.  _Proc. ACM Program. Lang._ 7, PLDI, Article 186 (jun 2023), 24 pages.  https://doi.org/10.1145/3591300
  * Cassez et al. (2023) Franck Cassez, Joanne Fuller, Milad K. Ghale, David J. Pearce, and Horacio Mijail Anton Quiles. 2023.  Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. In _FM_.
  * Chakarov et al. (2022) Aleksandar Chakarov, Aleksandr Fedchin, Zvonimir Rakamaric, and Neha Rungta. 2022.  Better Counterexamples for Dafny. In _TACAS_ _(Lecture Notes in Computer Science, Vol. 13243)_ , Dana Fisman and Grigore Rosu (Eds.). Springer, 404–411.  https://doi.org/10.1007/978-3-030-99524-9_23
  * Chakraborty and Ray (2021) Saikat Chakraborty and Baishakhi Ray. 2021.  On Multi-Modal Learning of Editing Source Code. In _36th IEEE/ACM International Conference on Automated Software Engineering, ASE 2021, Melbourne, Australia, November 15-19, 2021_. IEEE, 443–455.  https://doi.org/10.1109/ASE51524.2021.9678559
  * Chen et al. (2023) Zekai Chen, Mariann Micsinai Balan, and Kevin Brown. 2023.  Boosting Transformers and Language Models for Clinical Prediction in Immunotherapy. In _Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 5: Industry Track)_ , Sunayana Sitaram, Beata Beigman Klebanov, and Jason D Williams (Eds.). Association for Computational Linguistics, Toronto, Canada, 332–340.  https://doi.org/10.18653/v1/2023.acl-industry.32
  * CodeWhisperer (2023) Amazon CodeWhisperer. 2023.  Amazon CodeWhisperer.  https://aws.amazon.com/codewhisperer/.  [Online], [Accessed: 2023-09-20].
  * CompCert (2023) CompCert. 2023.  CompCert.  https://github.com/AbsInt/CompCert.  [Online], [Accessed: 2023-09-20].
  * Cook (2018) Byron Cook. 2018.  Formal Reasoning About the Security of Amazon Web Services. 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_ _(Lecture Notes in Computer Science, Vol. 10981)_ , Hana Chockler and Georg Weissenbacher (Eds.). Springer, 38–47.  https://doi.org/10.1007/978-3-319-96145-3_3
  * Copilot (2023) GitHub Copilot. 2023.  GitHub Copilot.  https://github.com/features/copilot.  [Online], [Accessed: 2023-09-20].
  * Cunningham et al. (2022) Garett Cunningham, Razvan C. Bunescu, and David Juedes. 2022.  Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs.  (2022), 25–32.  https://aclanthology.org/2022.mathnlp-1.4.pdf
  * Czajka and Kaliszyk (2018) Lukasz Czajka and Cezary Kaliszyk. 2018.  Hammer for Coq: Automation for Dependent Type Theory.  _J. Autom. Reason._ 61, 1-4 (2018), 423–453.  https://doi.org/10.1007/S10817-018-9458-4
  * Dafny (2023) Dafny. 2023.  dafny-lang.  https://github.com/dafny-lang/dafny.  [Online], [Accessed: 2023-09-20].
  * Dang et al. (2022) Hai Dang, Lukas Mecke, Florian Lehmann, Sven Goller, and Daniel Buschek. 2022.  How to Prompt? Opportunities and Challenges of Zero- and Few-Shot Learning for Human-AI Interaction in Creative Applications of Generative Models. In _Generative AI and HCI Workshop at CHI 2022_.  https://doi.org/10.48550/arXiv.2209.01390
  * de Moura and Bjørner (2008) Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008.  Z3: An Efficient SMT Solver. In _TACAS_. 337–340.  https://doi.org/10.1007/978-3-540-78800-3_24
  * Deckers et al. (2023) Niklas Deckers, Maik Fröbe, Johannes Kiesel, Gianluca Pandolfo, Christopher Schröder, Benno Stein, and Martin Potthast. 2023.  The Infinite Index: Information Retrieval on Generative Text-To-Image Models. In _CHIIR_. Association for Computing Machinery, New York, NY, USA.  https://doi.org/10.1145/3576840.3578327
  * Erbsen et al. (2020) Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2020.  Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises.  _ACM SIGOPS Oper. Syst. Rev._ 54, 1 (2020), 23–30.  https://doi.org/10.1145/3421473.3421477
  * Faria and Abreu (2023) João Pascoal Faria and Rui Abreu. 2023.  Case Studies of Development of Verified Programs with Dafny for Accessibility Assessment. In _Fundamentals of Software Engineering - 10th International Conference, FSEN 2023, Tehran, Iran, May 4-5, 2023, Revised Selected Papers_ _(Lecture Notes in Computer Science, Vol. 14155)_ , Hossein Hojjat and Erika Ábrahám (Eds.). Springer, 25–39.  https://doi.org/10.1007/978-3-031-42441-0_3
  * Feldt and Magazinius (2010) Robert Feldt and Ana Magazinius. 2010.  Validity Threats in Empirical Software Engineering Research - An Initial Survey. In _Proceedings of the 22nd International Conference on Software Engineering & Knowledge Engineering (SEKE’2010), Redwood City, San Francisco Bay, CA, USA, July 1 - July 3, 2010_. Knowledge Systems Institute Graduate School, 374–379.
  * First and Brun (2022) Emily First and Yuriy Brun. 2022.  Diversity-Driven Automated Formal Verification. In _44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022_. ACM, 1–13.  https://doi.org/10.1145/3510003.3510138
  * First et al. (2020) Emily First, Yuriy Brun, and Arjun Guha. 2020.  TacTok: semantics-aware proof synthesis.  _Proc. ACM Program. Lang._ 4, OOPSLA (2020), 231:1–231:31.  https://doi.org/10.1145/3428299
  * First et al. (2023) Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023.  Baldur: Whole-Proof Generation and Repair with Large Language Models. In _Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2023, San Francisco, CA, USA, December 3-9, 2023_ , Satish Chandra, Kelly Blincoe, and Paolo Tonella (Eds.). ACM, 1229–1241.  https://doi.org/10.1145/3611643.3616243
  * França et al. (2011) Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. 2011.  Towards Formally Verified Optimizing Compilation in Flight Control Software. In _Bringing Theory to Practice: Predictability and Performance in Embedded Systems_ , Philipp Lucas, Lothar Thiele, Benoit Triquet, Theo Ungerer, and Reinhard Wilhelm (Eds.), Vol. 18. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 59–68.  https://doi.org/10.4230/OASIcs.PPES.2011.59
  * Frieder et al. (2023) Simon Frieder, Luca Pinchetti, Ryan-Rhys Griffiths, Tommaso Salvatori, Thomas Lukasiewicz, Philipp Christian Petersen, Alexis Chevalier, and Julius Berner. 2023.  Mathematical Capabilities of ChatGPT.  _CoRR_ abs/2301.13867 (2023).  https://doi.org/10.48550/arXiv.2301.13867
  * Galitsky (2023) Boris A. Galitsky. 2023.  Truth-O-Meter: Collaborating with LLM in Fighting its Hallucinations.  _Preprints_ (2023).  https://doi.org/10.20944/preprints202307.1723.v1
  * Garavel et al. (2020) Hubert Garavel, Maurice H Ter Beek, and Jaco Van De Pol. 2020.  The 2020 expert survey on formal methods. In _International Conference on Formal Methods for Industrial Critical Systems_. Springer, 3–69.
  * GCC (2023) GCC. 2023.  GCC, the GNU Compiler Collection.  https://gcc.gnu.org/.  [Online], [Accessed: 2023-09-20].
  * Greengard (2021) Samuel Greengard. 2021.  _The Internet of Things_.  MIT press.
  * Gulwani et al. (2017) Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. 2017.  Program Synthesis.  _Founds. Trends. Prog. Lang._ 4, 1-2 (2017), 1–119.  https://doi.org/10.1561/2500000010
  * Hallgren (2012) Kevin A Hallgren. 2012.  Computing inter-rater reliability for observational data: an overview and tutorial.  _Tutorials in quantitative methods for psychology_ 8, 1 (2012), 23.
  * Hawblitzel et al. (2015) Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath T. V. Setty, and Brian Zill. 2015.  IronFleet: proving practical distributed systems correct. In _SOSP_ , Ethan L. Miller and Steven Hand (Eds.). ACM, 1–17.  https://doi.org/10.1145/2815400.2815428
  * Hawblitzel et al. (2014) Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014.  Ironclad Apps: End-to-End Security via Automated Full-System Verification. In _11th USENIX Symposium on Operating Systems Design and Implementation, OSDI ’14, Broomfield, CO, USA, October 6-8, 2014_ , Jason Flinn and Hank Levy (Eds.). USENIX Association, 165–181.  https://www.usenix.org/conference/osdi14/technical-sessions/presentation/hawblitzel
  * Hoare (1969) C. A. R. Hoare. 1969.  An Axiomatic Basis for Computer Programming.  _Commun. ACM_ 12, 10 (1969), 576–580.  https://doi.org/10.1145/363235.363259
  * Hou et al. (2022) Yutai Hou, Hongyuan Dong, Xinghao Wang, Bohan Li, and Wanxiang Che. 2022.  MetaPrompting: Learning to Learn Better Prompts. In _Proceedings of the 29th International Conference on Computational Linguistics, COLING 2022, Gyeongju, Republic of Korea, October 12-17, 2022_ , Nicoletta Calzolari, Chu-Ren Huang, Hansaem Kim, James Pustejovsky, Leo Wanner, Key-Sun Choi, Pum-Mo Ryu, Hsin-Hsi Chen, Lucia Donatelli, Heng Ji, Sadao Kurohashi, Patrizia Paggio, Nianwen Xue, Seokhwan Kim, Younggyun Hahm, Zhong He, Tony Kyungil Lee, Enrico Santus, Francis Bond, and Seung-Hoon Na (Eds.). International Committee on Computational Linguistics, 3251–3262.  https://aclanthology.org/2022.coling-1.287
  * Irfan et al. (2022) Ahmed Irfan, Sorawee Porncharoenwase, Zvonimir Rakamaric, Neha Rungta, and Emina Torlak. 2022.  Testing Dafny (experience paper). In _ISSTA ’22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18 - 22, 2022_ , Sukyoung Ryu and Yannis Smaragdakis (Eds.). ACM, 556–567.  https://doi.org/10.1145/3533767.3534382
  * Jacobs and 2020 (2023) Kevin Jacobs and Benjamin Beurdouche. 2020. 2023.  Performance Improvements via Formally-Verified Cryptography in Firefox.  https://blog.mozilla.org/security/2020/07/06/performance-improvements-viaformally-verified-cryptography-in-firefox/.  [Online], [Accessed: 2023-09-20].
  * Jiang et al. (2022a) Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygózdz, Piotr Milos, Yuhuai Wu, and Mateja Jamnik. 2022a.  Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In _Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022_ , Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (Eds.).  http://papers.nips.cc/paper_files/paper/2022/hash/377c25312668e48f2e531e2f2c422483-Abstract-Conference.html
  * Jiang et al. (2022b) Ellen Jiang, Kristen Olson, Edwin Toh, Alejandra Molina, Aaron Donsbach, Michael Terry, and Carrie J Cai. 2022b.  PromptMaker: Prompt-Based Prototyping with Large Language Models. In _CHI_. Article 35, 8 pages.  https://doi.org/10.1145/3491101.3503564
  * Jones and Misra (2021) Cliff B Jones and Jayadev Misra. 2021.  _Theories of Programming: The Life and Works of Tony Hoare_.  Morgan & Claypool.
  * Klein et al. (2009) Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009.  seL4: formal verification of an OS kernel.. In _SOSP_. 207–220.  https://doi.org/10.1145/1629575.1629596
  * Kulal et al. (2019) Sumith Kulal, Panupong Pasupat, Kartik Chandra, Mina Lee, Oded Padon, Alex Aiken, and Percy Liang. 2019.  SPoC: Search-based Pseudocode to Code. In _Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada_ , Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d’Alché-Buc, Emily B. Fox, and Roman Garnett (Eds.). 11883–11894.
  * Le Goues et al. (2011) Claire Le Goues, K Rustan M Leino, and Michał Moskal. 2011.  The Boogie verification debugger.  _SEFM, LNCS_ 7041 (2011), 407–414.
  * Leino (2017) K. Rustan M. Leino. 2017.  Accessible Software Verification with Dafny.  _IEEE Softw._ 34, 6 (2017), 94–97.  https://doi.org/10.1109/MS.2017.4121212
  * Leino (2020) K. Rustan M. Leino. 2020.  _Program Proofs_.  Available from Lulu.com.
  * Leino and Nelson (1998) K. Rustan M. Leino and Greg Nelson. 1998.  An extended static checker for Modula-3. In _International Conference on Compiler Construction_. Springer, 302–305.
  * Leroy (2009) Xavier Leroy. 2009.  Formal verification of a realistic compiler.  _Commun. ACM_ 52, 7 (2009), 107–115.  https://doi.org/10.1145/1538788.1538814
  * Li et al. (2022a) Lingwei Li, Li Yang, Huaxi Jiang, Jun Yan, Tiejian Luo, Zihan Hua, Geng Liang, and Chun Zuo. 2022a.  AUGER: automatically generating review comments with pre-training models. In _ESEC/FSE_ , Abhik Roychoudhury, Cristian Cadar, and Miryung Kim (Eds.). ACM, 1009–1021.  https://doi.org/10.1145/3540250.3549099
  * Li et al. (2022b) Liyi Li, Mingwei Zhu, Yi Lee, Le Chang, and Xiaodi Wu. 2022b.  Quantum Natural Proof: A New Perspective of Hybrid Quantum-Classical Program Verification.  _CoRR_ abs/2211.06411 (2022).  https://doi.org/10.48550/arXiv.2211.06411
  * Li et al. (2023) Yifei Li, Zeqi Lin, Shizhuo Zhang, Qiang Fu, Bei Chen, Jian-Guang Lou, and Weizhu Chen. 2023.  Making Language Models Better Reasoners with Step-Aware Verifier. In _Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)_ , Anna Rogers, Jordan Boyd-Graber, and Naoaki Okazaki (Eds.). Association for Computational Linguistics, Toronto, Canada, 5315–5333.  https://doi.org/10.18653/v1/2023.acl-long.291
  * Liu and Chilton (2022) Vivian Liu and Lydia B Chilton. 2022.  Design Guidelines for Prompt Engineering Text-to-Image Generative Models. In _CHI_. Article 384, 23 pages.  https://doi.org/10.1145/3491102.3501825
  * LLVM (2023) LLVM. 2023.  The LLVM Compiler Infrastructure.  https://llvm.org/.  [Online], [Accessed: 2023-09-20].
  * Madaan et al. (2022) Aman Madaan, Shuyan Zhou, Uri Alon, Yiming Yang, and Graham Neubig. 2022.  Language Models of Code are Few-Shot Commonsense Learners. In _EMNLP_ , Yoav Goldberg, Zornitsa Kozareva, and Yue Zhang (Eds.). Association for Computational Linguistics, 1384–1403.
  * Mark Chen et al. (2021) Mark Chen et al. 2021.  Evaluating Large Language Models Trained on Code.  _CoRR_ abs/2107.03374 (2021).  https://arxiv.org/abs/2107.03374
  * Mashhadi and Hemmati (2021) Ehsan Mashhadi and Hadi Hemmati. 2021.  Applying CodeBERT for Automated Program Repair of Java Simple Bugs. In _MSR_. 505–509.  https://doi.org/10.1109/MSR52588.2021.00063
  * Mastropaolo et al. (2023) Antonio Mastropaolo, Nathan Cooper, David Nader-Palacio, Simone Scalabrino, Denys Poshyvanyk, Rocco Oliveto, and Gabriele Bavota. 2023.  Using Transfer Learning for Code-Related Tasks.  _IEEE Trans. Software Eng._ 49, 4 (2023), 1580–1598.  https://doi.org/10.1109/TSE.2022.3183297
  * McKenna et al. (2023) Nick McKenna, Tianyi Li, Liang Cheng, Mohammad Javad Hosseini, Mark Johnson, and Mark Steedman. 2023.  Sources of Hallucination by Large Language Models on Inference Tasks. In _Findings of the Association for Computational Linguistics: EMNLP 2023, Singapore, December 6-10, 2023_ , Houda Bouamor, Juan Pino, and Kalika Bali (Eds.). Association for Computational Linguistics, 2758–2774.  https://aclanthology.org/2023.findings-emnlp.182
  * Meadows and Freitas (2022) Jordan Meadows and André Freitas. 2022.  A Survey in Mathematical Language Processing.  _CoRR_ abs/2205.15231 (2022).  https://doi.org/10.48550/arXiv.2205.15231
  * Microsoft (2023a) Microsoft. 2023a.  The Dafny Programming and Verification Language.  https://dafny.org/.  [Online], [Accessed: 2023-09-20].
  * Microsoft (2023b) Microsoft. 2023b.  Microsoft Research.  https://www.microsoft.com/en-us/research/.  [Online], [Accessed: 2023-09-20].
  * Murray et al. (2013) Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. 2013.  seL4: From General Purpose to a Proof of Information Flow Enforcement. In _S &P_. 415–429.  https://doi.org/10.1109/SP.2013.35
  * Nashid et al. (2023) Noor Nashid, Mifta Sintaha, and Ali Mesbah. 2023.  Retrieval-Based Prompt Selection for Code-Related Few-Shot Learning. In _ICSE_.
  * Nederpelt et al. (1994) R.P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer (Eds.). 1994.  _Selected Papers on Automath_.  North Holland.
  * Noble et al. (2022) James Noble, David Streader, Isaac Oscar Gariano, and Miniruwani Samarakoon. 2022.  More Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme. In _NASA Symposium on Formal Methods_.
  * OpenAI (2023a) OpenAI. 2023a.  GPT-4 Technical Report.  _CoRR_ abs/2303.08774 (2023).  https://doi.org/10.48550/arXiv.2303.08774
  * OpenAI (2023b) OpenAI. 2023b.  OpenAI.  https://platform.openai.com/docs/models.  [Online], [Accessed: 2023-09-20].
  * Qiao et al. (2023) Shuofei Qiao, Yixin Ou, Ningyu Zhang, Xiang Chen, Yunzhi Yao, Shumin Deng, Chuanqi Tan, Fei Huang, and Huajun Chen. 2023.  Reasoning with Language Model Prompting: A Survey. In _Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2023, Toronto, Canada, July 9-14, 2023_ , Anna Rogers, Jordan L. Boyd-Graber, and Naoaki Okazaki (Eds.). Association for Computational Linguistics, 5368–5393.  https://doi.org/10.18653/V1/2023.ACL-LONG.294
  * Radford et al. (2018) Alec Radford, Karthik Narasimhan, Tim Salimans, Ilya Sutskever, et al. 2018\.  Improving language understanding by generative pre-training.  OpenAI.com.
  * Reynolds and McDonell (2021) Laria Reynolds and Kyle McDonell. 2021.  Prompt Programming for Large Language Models: Beyond the Few-Shot Paradigm. In _Extended Abstracts of the 2021 CHI Conference on Human Factors in Computing Systems_. Article 314, 7 pages.  https://doi.org/10.1145/3411763.3451760
  * Ringer et al. (2019) Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. 2019.  QED at Large: A Survey of Engineering of Formally Verified Software.  _Founds. Trends. Prog. Lang._ 5, 2-3 (2019), 102–281.  https://doi.org/10.1561/2500000045
  * Rohan Anil et al. (2023) Rohan Anil et al. 2023.  PaLM 2 Technical Report.  _CoRR_ abs/2305.10403 (2023).
  * Rozière et al. (2023) Baptiste Rozière, Jonas Gehring, Fabian Gloeckle, Sten Sootla, Itai Gat, Xiaoqing Ellen Tan, Yossi Adi, Jingyu Liu, Tal Remez, Jérémy Rapin, et al. 2023\.  Code llama: Open foundation models for code.  _arXiv preprint arXiv:2308.12950_ (2023).
  * Salvagno and Taccone (2023) M. Salvagno and A.G. Taccone, F.S.and Gerli. 2023.  Artificial intelligence hallucinations.  _Crit Care_ (2023).  https://doi.org/10.1186/s13054-023-04473-y
  * Sanchez-Stern et al. (2020) Alex Sanchez-Stern, Yousef Alhessi, Lawrence K. Saul, and Sorin Lerner. 2020.  Generating correctness proofs with neural networks. In _Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, MAPL@PLDI 2020, London, UK, June 15, 2020_ , Koushik Sen and Mayur Naik (Eds.). ACM, 1–10.  https://doi.org/10.1145/3394450.3397466
  * Sanchez-Stern et al. (2023) Alex Sanchez-Stern, Emily First, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, and Talia Ringer. 2023.  Passport: Improving Automated Formal Verification Using Identifiers.  _ACM Trans. Program. Lang. Syst._ 45, 2 (2023), 12:1–12:30.  https://doi.org/10.1145/3593374
  * seL4 Project (2023) seL4 Project. 2023.  The seL4® Microkernel.  https://sel4.systems/.  [Online], [Accessed: 2023-09-20].
  * Siegmund et al. (2015) Janet Siegmund, Norbert Siegmund, and Sven Apel. 2015.  Views on Internal and External Validity in Empirical Software Engineering. In _37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16-24, 2015, Volume 1_ , Antonia Bertolino, Gerardo Canfora, and Sebastian G. Elbaum (Eds.). IEEE Computer Society, 9–19.  https://doi.org/10.1109/ICSE.2015.24
  * Sintaha et al. (2023) Mifta Sintaha, Noor Nashid, and Ali Mesbah. 2023.  Katana: Dual Slicing Based Context for Learning Bug Fixes.  _ACM Trans. Softw. Eng. Methodol._ 32, 4 (2023), 100:1–100:27.  https://doi.org/10.1145/3579640
  * Tufano et al. (2022a) Michele Tufano, Shao Kun Deng, Neel Sundaresan, and Alexey Svyatkovskiy. 2022a.  METHODS2TEST: A dataset of focal methods mapped to test cases. In _19th IEEE/ACM International Conference on Mining Software Repositories, MSR 2022, Pittsburgh, PA, USA, May 23-24, 2022_. ACM, 299–303.  https://doi.org/10.1145/3524842.3528009
  * Tufano et al. (2019) Michele Tufano, Cody Watson, Gabriele Bavota, Massimiliano Di Penta, Martin White, and Denys Poshyvanyk. 2019.  An Empirical Study on Learning Bug-Fixing Patches in the Wild via Neural Machine Translation.  _ACM Trans. Softw. Eng. Methodol._ 28, 4 (2019), 19:1–19:29.  https://doi.org/10.1145/3340544
  * Tufano et al. (2022b) Rosalia Tufano, Simone Masiero, Antonio Mastropaolo, Luca Pascarella, Denys Poshyvanyk, and Gabriele Bavota. 2022b.  Using Pre-Trained Models to Boost Code Review Automation. In _44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022_. ACM, 2291–2302.  https://doi.org/10.1145/3510003.3510621
  * Tufano et al. (2023) Rosalia Tufano, Luca Pascarella, and Gabriele Bavota. 2023.  Automating Code-Related Tasks Through Transformers: The Impact of Pre-training. In _45th IEEE/ACM International Conference on Software Engineering, ICSE 2023, Melbourne, Australia, May 14-20, 2023_. IEEE, 2425–2437.  https://doi.org/10.1109/ICSE48619.2023.00203
  * Viera et al. (2005) Anthony J Viera, Joanne M Garrett, et al. 2005\.  Understanding interobserver agreement: the kappa statistic.  _Fam med_ 37, 5 (2005), 360–363.
  * Wang et al. (2023) Yue Wang, Hung Le, Akhilesh Deepak Gotmare, Nghi D. Q. Bui, Junnan Li, and Steven C. H. Hoi. 2023.  CodeT5+: Open Code Large Language Models for Code Understanding and Generation.  _CoRR_ abs/2305.07922 (2023).
  * Wang et al. (2021) Y. Wang, W. Wang, S.R. Joty, and S.C.H. Hoi. 2021.  CodeT5: Identifier-aware Unified Pre-trained Encoder-Decoder Models for Code Understanding and Generation. In _EMNLP_.  https://doi.org/10.18653/v1/2021.emnlp-main.685
  * Watson et al. (2022) Cody Watson, Nathan Cooper, David Nader-Palacio, Kevin Moran, and Denys Poshyvanyk. 2022.  A Systematic Literature Review on the Use of Deep Learning in Software Engineering Research.  _ACM Trans. Softw. Eng. Methodol._ 31, 2 (2022), 32:1–32:58.  https://doi.org/10.1145/3485275
  * Wayne (2018) Hillel Wayne. 2018.  Temporal Logic.  In _Practical TLA+_. Springer, 97–110.
  * Wei et al. (2022) Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi, Quoc V. Le, and Denny Zhou. 2022.  Chain-of-Thought Prompting Elicits Reasoning in Large Language Models. In _Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022_ , Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (Eds.).  http://papers.nips.cc/paper_files/paper/2022/hash/9d5609613524ecf4f15af0f7b31abca4-Abstract-Conference.html
  * Wu et al. (2022) Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022.  Autoformalization with Large Language Models. In _NeurIPS_.
  * Yang and Deng (2019) Kaiyu Yang and Jia Deng. 2019.  Learning to Prove Theorems via Interacting with Proof Assistants. In _Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA_ _(Proceedings of Machine Learning Research, Vol. 97)_ , Kamalika Chaudhuri and Ruslan Salakhutdinov (Eds.). PMLR, 6984–6994.  http://proceedings.mlr.press/v97/yang19a.html
  * Yang et al. (2011) Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011.  Finding and understanding bugs in C compilers. In _Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011_ , Mary W. Hall and David A. Padua (Eds.). ACM, 283–294.  https://doi.org/10.1145/1993498.1993532
  * Yang et al. (2022) Yanming Yang, Xin Xia, David Lo, and John C. Grundy. 2022.  A Survey on Deep Learning for Software Engineering.  _ACM Comput. Surv._ 54, 10s (2022), 206:1–206:73.  https://doi.org/10.1145/3505243
  * Yang et al. (2023) Zhenkun Yang, Wen Wang, Jeremy Casas, Pasquale Cocchini, and Jin Yang. 2023.  Towards A Correct-by-Construction FHE Model.  _IACR Cryptol. ePrint Arch._ (2023), 281.
  * Yasunaga and Liang (2020) Michihiro Yasunaga and Percy Liang. 2020.  Graph-based, Self-Supervised Program Repair from Diagnostic Feedback. In _Proceedings of the 37th International Conference on Machine Learning, ICML 2020, 13-18 July 2020, Virtual Event_ _(Proceedings of Machine Learning Research, Vol. 119)_. PMLR, 10799–10808.  http://proceedings.mlr.press/v119/yasunaga20a.html
  * Zhou et al. (2022) Hattie Zhou, Azade Nova, Hugo Larochelle, Aaron C. Courville, Behnam Neyshabur, and Hanie Sedghi. 2022.  Teaching Algorithmic Reasoning via In-context Learning.  _CoRR_ abs/2211.09066 (2022).  https://doi.org/10.48550/arXiv.2211.09066