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.

翻译：本研究思路论文提出利用大型语言模型（LLMs）来提升Dafny开发者的生产力。尽管在过去十年中，Dafny等验证感知语言的使用显著增加，但其仍未得到广泛采用。使用此类语言的成本往往过高，原因在于开发者需要具备较高的专业水平，且在尝试证明程序正确性时常面临挑战。尽管Dafny自动化了大量验证过程，但有时仍存在过于复杂的步骤，需其独立完成。例如，缺失引理的情况——即Dafny在缺乏额外定理辅助证明步骤时无法证明某个结果。本文描述了一项初步工作：开发一个新的Dafny插件，利用LLMs协助开发者，通过生成相关引理建议（Dafny无法自主发现和使用的引理）。此外，对于无法自动证明的引理，该插件还尝试提供配套的计算式证明。我们还讨论了未来工作的设想，通过提出一项研究路线图：利用LLMs提高验证感知语言的整体采用率，通过提升开发者生产力并降低形式化规约编写及程序属性证明所需的专业门槛。