Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Leveraging Large Language Models to Boost Dafny's Developers Productivity

Álvaro Silva, Alexandra Mendes, João F. Ferreira

TL;DR

The paper addresses the barrier to adopting verification-aware languages like Dafny due to high expertise and proof burdens. It proposes a Dafny–LLM plugin that generates lemmas, calculational proofs, repairs, and natural-language specifications, with a continuous verifier–LLM feedback loop to refine outputs. Preliminary GPT-4 experiments show promising lemma inference but underscore the need for carefully designed prompts and preconditions to ensure provability, as well as more robust proof inference. The work outlines a research agenda including dataset expansion (CloverBench), specialized Dafny datasets, and VS Code integration to enhance developer productivity and wider adoption of formal verification tooling.

Abstract

This research idea paper proposes leveraging Large Language Models (LLMs) to enhance the productivity of Dafny developers. Although the use of verification-aware languages, such as Dafny, has increased considerably in the last decade, these are still not widely adopted. Often the cost of using such languages is too high, due to the level of expertise required from the developers and challenges that they often face when trying to prove a program correct. Even though Dafny automates a lot of the verification process, sometimes there are steps that are too complex for Dafny to perform on its own. One such case is that of missing lemmas, i.e. Dafny is unable to prove a result without being given further help in the form of a theorem that can assist it in the proof of the step. In this paper, we describe preliminary work on a new Dafny plugin that leverages LLMs to assist developers by generating suggestions for relevant lemmas that Dafny is unable to discover and use. Moreover, for the lemmas that cannot be proved automatically, the plugin also attempts to provide accompanying calculational proofs. We also discuss ideas for future work by describing a research agenda on using LLMs to increase the adoption of verification-aware languages in general, by increasing developers productivity and by reducing the level of expertise required for crafting formal specifications and proving program properties.

Leveraging Large Language Models to Boost Dafny's Developers Productivity

TL;DR

The paper addresses the barrier to adopting verification-aware languages like Dafny due to high expertise and proof burdens. It proposes a Dafny–LLM plugin that generates lemmas, calculational proofs, repairs, and natural-language specifications, with a continuous verifier–LLM feedback loop to refine outputs. Preliminary GPT-4 experiments show promising lemma inference but underscore the need for carefully designed prompts and preconditions to ensure provability, as well as more robust proof inference. The work outlines a research agenda including dataset expansion (CloverBench), specialized Dafny datasets, and VS Code integration to enhance developer productivity and wider adoption of formal verification tooling.

Abstract

This research idea paper proposes leveraging Large Language Models (LLMs) to enhance the productivity of Dafny developers. Although the use of verification-aware languages, such as Dafny, has increased considerably in the last decade, these are still not widely adopted. Often the cost of using such languages is too high, due to the level of expertise required from the developers and challenges that they often face when trying to prove a program correct. Even though Dafny automates a lot of the verification process, sometimes there are steps that are too complex for Dafny to perform on its own. One such case is that of missing lemmas, i.e. Dafny is unable to prove a result without being given further help in the form of a theorem that can assist it in the proof of the step. In this paper, we describe preliminary work on a new Dafny plugin that leverages LLMs to assist developers by generating suggestions for relevant lemmas that Dafny is unable to discover and use. Moreover, for the lemmas that cannot be proved automatically, the plugin also attempts to provide accompanying calculational proofs. We also discuss ideas for future work by describing a research agenda on using LLMs to increase the adoption of verification-aware languages in general, by increasing developers productivity and by reducing the level of expertise required for crafting formal specifications and proving program properties.
Paper Structure (11 sections, 2 figures)

This paper contains 11 sections, 2 figures.

Table of Contents

  1. Introduction
  2. Synergies between Dafny and LLMs
  3. Predicate and Lemma Inference
  4. Proof Inference
  5. Automated Repair
  6. Summarization and Natural Language Specs
  7. Preliminary Experiments
  8. Lemma Inference
  9. Proof Inference
  10. Related Work
  11. Conclusion

Figures (2)

  • Figure 1: GPT-4 suggests lemmas to complete method verification.
  • Figure 2: GPT-4-generated proof for lemma .