Automatic Generation of Loop Invariants in Dafny with Large Language Models

• Type: Article in International Conference Proceedings Book
• Date: 2025

Authors

João Pascoal Faria (Author) FEUP; Trigo, E (Author) Other; Rui Abreu (Author) FEUP

Conference proceedings International

Title: Lecture Notes in Computer Science

Pages: 138-154

11th IFIP WG 2.2 International Conference on Fundamentals of Software Engineering, FSEN 2025

Västerås, 7 April 2025 through 8 April 2025

Indexing

Scopus - 0 Citations

Other information

Authenticus ID: P-018-G5G

DOI: 10.1007/978-3-031-87054-5_10

Abstract (EN): Recent verification tools aim to make formal verification more accessible for software engineers by automating most of the verification process. However, the manual work and expertise required to write verification helper code, such as loop invariants and auxiliary lemmas and assertions, remains a barrier. This paper explores the use of Large Language Models (LLMs) to automate the generation of loop invariants for programs in Dafny. We tested the approach on a curated dataset of 100 programs in Dafny involving arrays, strings, and numeric types. Using a multimodel approach that combines GPT-4o and Claude 3.5 Sonnet, correct loop invariants (passing the Dafny verifier) were generated at the first attempt for 92% of the programs, and in at most five attempts for 95% of the programs. Additionally, we developed an extension to the Dafny plugin for Visual Studio Code to incorporate automatic loop invariant generation into the IDE. Our work stands out from related approaches by handling a broader class of problems and offering IDE integration. © IFIP International Federation for Information Processing 2025.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 16