Leveraging Large Language Models to Boost Dafny’s Developers Productivity

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked page and section references, both figures, footnotes, every quotation, the lemma statements and the false-lemma counterexample, and the Verus sketches; corrected claims that the trials were run by hand, that the 3 lemmas were proved zero times, that the paper does not link the missing preconditions to the proof failures, the unmarked falsity inference, the unsupported claims about later work, and the fifth requires line attributed to the paper; Verus sketches left unchanged and unchecked (exists over p * q may have no usable trigger).

source: Álvaro Silva, Alexandra Mendes, João F. Ferreira, arXiv:2401.00963v1 (1 Jan 2024), 5 pages (4 of text, 1 of references), no appendix.

what kind of paper this is

It is a plan plus two worked examples, and it says so: “This research idea paper proposes leveraging Large Language Models (LLMs) to enhance the productivity of Dafny developers.” (Abstract, p.1) Nothing is measured over a set of programs. There are two preliminary trials with one model, “the latest version of GPT-4 Turbo, gpt-4-1106-preview, trained on data up to April 2023, enabling support for contexts with 128,000 tokens” (Section 3, p.2; the quoted words are the end of a sentence):

• one method whose loop invariant fails, for which GPT-4 proposed three helper lemmas and where to call them (Section 3.1, Figure 1, p.3)
• one number-theory lemma, for which GPT-4 wrote a calculational proof after heavy prompting (Section 3.2, Figure 2, p.4)

Denominators: 1 program, 3 lemma statements proposed, none of the 3 shown proved (the paper says they cannot be proved as stated, Section 3.1), 1 separate lemma proved after two manual edits. No success rate, no repetition, no count of prompts tried.

What stays trusted in the first trial: the three lemmas themselves. They are used without proofs; the paper says they cannot be proved as stated, and Inference: they are false (see technique 2).

The premise the whole plan rests on: “LLMs and Dafny verification capabilities can complement each other, as LLMs are inherently creative but not always reliable, whilst Dafny’s verification engine acts as a stringent gatekeeper, ensuring that artifacts generated by LLMs undergo a rigorous verification process.” (Section 2, p.1)

technique 1: ask for helper lemmas at a failing loop invariant, with the verifier’s message written into the code

what it is: give the model the whole method, mark the invariant the verifier could not prove with a comment that carries the error text, and ask for lemma declarations plus the places to call them.

when to use: the postcondition follows from the invariants, but one invariant is not shown to be maintained because the solver lacks a fact about a library data type. In the paper’s case: “However, it cannot automatically prove the second invariant (identified by the red comment), because it is not able to automatically prove relevant properties about multisets.” (Section 3.1, p.3)

how it is done (Section 3.1 and Figure 1, p.3):

1. take the method with its contract and invariants; the example is CoincidenceCount from Leino’s book, which counts the common elements of two sorted arrays and ensures c == |multiset(a[..]) * multiset(b[..])|
2. above the failing invariant insert the comment the paper gives in footnote 2: // VERIFIER_ERROR loop invariant violation. This invariant could not be proved to be maintained by the loop //
3. send it with this prompt (Figure 1b, quoted whole): “You are a software expert specializing in formal methods using the Dafny programming language. You receive the following program where a loop invariant could not be proven. The verifier error message is inside // VERIFIER ERROR … //. Your task is to create lemmas and insert them into the code to facilitate verification.”
4. take from the answer the lemma signatures with requires/ensures and the call sites; GPT-4 returned three lemmas, one per way the loop advances (m only, n only, both), each relating the multiset intersection of the remaining suffixes before and after the step, and put one call at the start of each branch of the loop body
5. run the verifier on the program with the lemmas left without bodies; correct by hand what fails

The result in the paper’s words: “Only a small correction was required to make the program verify using these lemmas as axioms (highlighted in blue).” (Section 3.1, p.3) The correction was to the both-advance lemma: GPT-4 wrote that the intersection size is unchanged; the right statement adds + 1 (Figure 1c).

The shape of what the model found, which is the reusable part (Inference): the failing invariant is c + |f(m, n)| == K. Each branch changes m, n or c. The lemma for a branch states how |f| changes under exactly that branch’s update, so that the invariant after the update follows by arithmetic. One lemma per branch, named after the update.

Verus form (Inference: the paper is about Dafny; a sketch, not run through Verus). The lemma is a proof fn with requires and ensures; the call goes in a proof { } block inside the loop body, before the assignment it justifies; the fact it must restore is the loop’s invariant clause. Ghost values of the arrays are their views as Seq:

proof fn lemma_intersection_after_increase_m(a: Seq<int>, b: Seq<int>, m: int, n: int)
    requires
        0 <= m < a.len(),
        0 <= n <= b.len(),
        forall|i: int, j: int| 0 <= i < j < a.len() ==> a[i] <= a[j],
        forall|i: int, j: int| 0 <= i < j < b.len() ==> b[i] <= b[j],
        n < b.len() ==> a[m] < b[n],
    ensures
        common(a.subrange(m, a.len() as int), b.subrange(n, b.len() as int))
            == common(a.subrange(m + 1, a.len() as int), b.subrange(n, b.len() as int)),
{
    admit();
}

Here common stands for a spec fn giving the size of the multiset intersection, and admit() stands for the missing body. The fifth requires line is not in GPT-4’s lemma; it is the branch condition. Inference: the paper names the missing precondition only for the both-advance lemma and says similar annotations are needed for the others (technique 2). What changes from Dafny: Dafny’s if { case ... } with three guarded cases becomes an if/else if/else; a lemma called from executable code must be called in proof mode; the error text can be given as the verifier’s own output with the line it points to, so the comment trick is optional. What does not carry over: nothing structural.

evidence: one program, one model, an unknown number of tries. The conclusion adds a caution about the tries: “However, throughout the experiments, several responses contained syntax errors that proved challenging to rectify through reprompting.” (Section 5, p.4)

limits: see technique 2; the lemmas found were not true.

technique 2: check lemma statements as axioms first, and why this alone proves nothing

what it is: the order of work the trial followed. First see whether the program verifies when the proposed lemmas are assumed; only then try to prove the lemmas.

when to use: Inference: as a cheap filter. A lemma set under which the program still does not verify can be thrown away before any effort is spent on proofs.

how it is done (Section 3.1, p.3):

1. declare each lemma with its contract and no body; Dafny then treats it as an axiom
2. verify the calling method
3. if it verifies, the lemma statements are sufficient; they are not yet known to be true

Steps 4 and 5 are not in the paper as executed steps; the paper states the need for them: 4. prove each lemma (attempted in Section 3.2, where the paper calls the results for these three lemmas “not as successful”; no proof of them is shown) 5. when a proof cannot be found, suspect the statement: add the facts that hold at the call site as preconditions

The paper reports that the statements are too strong: “However, note that these lemmas cannot be proved since they require more information in the precondition (e.g. to prove LemmaIntersectionAfterIncrease_mn, it is required to add a[m] == b[n] as a precondition; similar annotations are needed for the other lemmas).” (Section 3.1, p.3)

Inference: “cannot be proved” understates it. The _m lemma as printed in Figure 1c claims that dropping a[m] never changes the intersection size, for any sorted a, b and any m, n in range. With a = [1], b = [1], m = 0, n = 0 the left side is 1 and the right side is 0. The lemma is false, so the program “verified” from a false axiom, and a false axiom can make any program verify. The trial therefore shows that the model placed calls of the right shape, not that the method was verified.

Inference: the general rule this example teaches is that a model asked to “create lemmas to facilitate verification” tends to leave out the path condition of the branch where the lemma is called. A mechanical fix is to add the guard of the enclosing branch (a[m] == b[n], a[m] < b[n], b[n] < a[m]) as a requires of the lemma called in it.

Verus form (Inference): step 1 is a proof fn whose body is admit() or assume(false); step 2 is running Verus on the caller. The filter is sound to use only if the final check rejects any remaining admit() or assume(...). A second cheap filter not in the paper: before trying to prove a proposed lemma, test its statement on small concrete inputs, which would have rejected _m at once.

evidence: the same single example.

technique 3: get a calculational proof by showing the model many calculations

what it is: prompt for a proof in Dafny’s calc form, a chain of expressions joined by == with a hint between each pair, after putting many example calculations in the prompt.

when to use: the lemma is an equational or arithmetic fact that a person would prove by rewriting in steps. The paper’s reason for the form: “Dafny supports calculational proofs (aka verified calculations), which are proofs by stepwise formula manipulation.” (Section 2.2, p.2)

how it is done (Section 3.2, p.3–4):

1. state the lemma with its contract; the example is Factor0(p, y, x), requiring exists a :: x == p*a and exists b :: y == p*b, ensuring IsFactor(p, y + x) where IsFactor(p, x) is exists q :: p * q == x
2. put a whole file of example calculations in the prompt: “To achieve this, we designed a prompt incorporating extensive Dafny code and examples; in particular we provided all the contents of the integration test file for calculations.” (Section 3.2, p.4); the file is Dafny’s Calculations.dfy test (footnote 4)
3. for a lemma that has siblings, include a finished proof of one sibling; of the three multiset lemmas the paper says the best result “was when we asked to prove one of the lemmas, but gave a complete proof of one of the other similar lemmas” (Section 3.2, p.3–4; the quoted words are the end of a sentence)
4. run the verifier on the answer and repair by hand

What GPT-4 produced for Factor0 (Figure 2, p.4): two witnesses, var a: pos := x / p; and var b: pos := y / p;, then calc { p * (a + b); == { arithmetic } p * a + p * b; == { definition of a and b } x + y; }.

The two repairs needed, both stated by the paper:

• the hints were prose, not Dafny: “Even though the hints are correct and make sense, they are not accepted by Dafny. Nevertheless, once we comment them, the proof is accepted.” (Section 3.2, p.4)
• the witnesses had to be taken from the existential, not computed by division; in Dafny 4.3.0 the authors “had to change the variable definitions to” var a :| x == p*a; var b :| y == p*b; (Section 3.2, p.4)

Verus form (Inference; a sketch, not run through Verus). calc! is the same construct; Dafny’s such-that assignment :| is choose; the witness for the conclusion’s exists must be shown by an assert that names it; the distributive step is nonlinear arithmetic, which Verus’s default solver mode does not try, so it needs by (nonlinear_arith):

spec fn is_factor(p: int, x: int) -> bool {
    exists|q: int| p * q == x
}

proof fn factor0(p: int, y: int, x: int)
    requires
        is_factor(p, x),
        is_factor(p, y),
    ensures
        is_factor(p, y + x),
{
    let a = choose|a: int| p * a == x;
    let b = choose|b: int| p * b == y;
    assert(p * (a + b) == p * a + p * b) by (nonlinear_arith);
    assert(p * (a + b) == y + x);
}

What changes: in Dafny the proof passed with both hints removed, so Dafny’s solver did the distributive step alone; in Verus that step is the one line that needs help. The paper’s pos subset type (integers >= 1) has no direct Verus counterpart; int with a requires on positivity, or nat, replaces it. What does not carry over: free-text hints inside the calculation. In calc! the braces after a step hold proof code, so a hint must be a lemma call or an assert.

Inference: both of GPT-4’s mistakes are of one kind, replacing a logical step by a computation or a comment that reads well. x / p is a correct witness mathematically, and proving that needs a division fact the solver was not given; choose needs nothing.

evidence: one lemma accepted after the two edits. For the three multiset lemmas of technique 1: “Our experiments with prompt engineering to infer proofs for the three lemmas shown in Figure 1c were not as successful.” and “In general, there were many syntactic errors and we had to provide many examples of proofs to generate plausible solutions.” (Section 3.2, p.3) No proof of those three is shown. The authors’ own reading: “On the other hand, the proof inference experiment revealed that only through a meticulously crafted prompt with rich examples could GPT-4 successfully complete the proofs.” (Section 5, p.4)

limits: Inference: the three multiset lemmas could not have been proved by any prompt, because as stated they are false (technique 2). Section 3.1 says the lemmas cannot be proved without more preconditions, but Section 3.2 and Section 5 do not tie the weak proof results to that. Inference: so the paper’s low opinion of proof inference rests partly on asking for proofs of false statements.

technique 4: add proof steps the verifier does not need, to make it faster

what it is: a claim taken from another paper, not tested here: “In addition, even though Dafny can often prove the lemmas on its own, it has been shown that, even in those cases, adding proof steps that are not absolutely necessary can reduce considerably the verification time [5].” (Section 2.2, p.2) Reference [5] is Cassez’s verification of the incremental Merkle tree algorithm.

how it is done: the paper gives no steps.

Verus form (Inference): intermediate asserts or a calc! chain inside a proof fn that already verifies, kept because they cut solver time. Whether this holds for Verus is not shown by this paper.

technique 5: the verify-and-re-prompt loop, as planned

what it is: the repair loop the authors intend to build, described in one sentence: “We will follow a continuous feedback loop between LLMs and the Dafny’s verifier, where the LLM produces proofs or fixes to proofs and, should these not verify, the feedback produced by Dafny is fed into the LLM to produce another suggestion.” (Section 2.3, p.2)

when to use, per the paper: proof repair “in at least two contexts: when the code changes and existing proofs become invalid and when the user or the LLM suggest a proof that does not verify” (Section 2.3, p.2; part of a longer sentence).

how it is done: not built in this paper; the paper does not describe the trials of Section 3 as using such a loop (nor whether they ran through the plugin), and re-prompting did not reliably fix syntax errors (Section 5, p.4).

One point in this section that later LLM-verification work often drops: a failed verification does not say which side is wrong. “In addition, in the context of Dafny, when a bug is detected, i.e. the program fails to verify, the issue can be due to an incorrect specification or an incorrect implementation.” (Section 2.3, p.2)

Verus form (Inference): the same loop with Verus’s error output; the paper adds nothing to its design.

the rest of the agenda (stated, not done)

• lemma and predicate inference by prompting, then by fine-tuning if prompting is not enough (Section 2.1, p.2)
• proof inference with models fine-tuned on proof data (Section 2.2, p.2)
• repair of specifications as well as implementations and proofs (Section 2.3, p.2)
• summaries of code and specifications, better error messages, and translation of natural-language requirements into Dafny (Section 2.4, p.2)
• a dataset: “At the time of writing, CloverBench contains only 60 small CS textbook examples.” (Section 5, p.4), which the authors plan to extend
• delivery inside Dafny’s VS Code plugin (Section 5, p.4)

Motivating figures the paper cites from others: in Cassez’s Merkle-tree development “almost 90% of the lines of code are proofs and function definitions used in the proofs” (Section 2, p.2; part of a sentence); developers spend “around 58% percent of their time on program comprehension activities” (Section 2.4, p.2; part of a sentence, the doubled “percent” is the paper’s).

where the paper is inconsistent

• Figure 1a, third branch (b[n] < a[m], which advances n), calls LemmaIntersectionAfterIncrease_m, the lemma about advancing m. The lemma LemmaIntersectionAfterIncrease_n is declared in Figure 1c and called nowhere in Figure 1a. As printed, the third branch has no fact about advancing n. Inference: most likely a slip in the figure, since the _m lemma says nothing about n + 1; the paper’s text does not comment on it.
• the abstract describes “preliminary work on a new Dafny plugin”; Sections 3 and 5 describe prompts to GPT-4 with no mention of the plugin, and the last sentence says the integration into the plugin has only started. No plugin behaviour is shown.
• Section 5 calls the lemma result “promising results, demonstrating GPT-4’s ability to infer lemmas with minor errors” (p.4; part of a sentence). One of three had a wrong conclusion (+ 1 missing) and all three lacked a needed precondition (Section 3.1). Inference: that makes each of them false; “minor” describes the size of the edit, not the effect.
• Section 4 says “Clover [36] is the only work that we are aware of on using LLMs in the context of Dafny.” (p.4) This dates the paper (January 2024).

what VL should not redo, and what is still worth taking

Inference: nothing here is a result to build on or to reproduce; it is an early sketch with GPT-4 Turbo. Three things are worth keeping because they cost nothing:

• the one-lemma-per-branch shape for an invariant that counts or sums over a shrinking suffix
• the rule that a lemma proposed for a branch must carry that branch’s guard as a precondition
• the warning that a program verifying under assumed lemmas was reported as success although the lemmas are false; a pipeline must count a lemma only when its own proof verifies

threat to VL’s product

Inference: none as a competitor. The paper has no system and no numbers. Its value is as a record of two failure modes of a 2023 model that a Verus agent should still guard against: lemma statements missing their path conditions, and proofs that replace a logical step by a plausible computation.

techniques for the catalog

• error-as-comment lemma request: mark the unprovable invariant with the verifier’s message in a comment and ask the model for lemma declarations and their call sites
• one lemma per loop branch: for an invariant over a shrinking suffix, state for each branch how the measured quantity changes under exactly that branch’s update
• axioms-first sufficiency check: verify the caller with bodiless lemmas to filter lemma sets, then prove each lemma, counting nothing until its own proof passes
• branch guard as lemma precondition: add the condition of the branch where a lemma is called to its requires, since the one example had the model omit it (an inference from a single case)
• sibling-proof and example-file prompting for calculations: put a file of calculational proofs and a finished proof of a similar lemma in the prompt before asking for a calc proof
• witness by such-that, not by computation: take an existential’s witness with :| (Verus choose) instead of computing it by division
• redundant proof steps for speed: keep intermediate steps the verifier does not need when they cut verification time (cited from Cassez, not tested)

Last edited: 2026-10-13