Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles

TL;DR

This work tackles the manual burden of producing formal specifications for Dafny by introducing a multimodel LLM workflow that generates pre/postconditions, loop invariants, and proof helpers from conventional code and test assertions. It leverages a generate–check–repair–minimize loop, with test assertions acting as specification oracles and the Dafny verifier providing automatic feedback, achieving a 98.2% success rate on 110 programs. The authors contribute TESTDAFNY110, a Dafny-focused annotation pipeline, and the Dafny AI Assistant IDE plugin, demonstrating strong specification quality (≈96% logical equivalence to expert specs) and practical usability improvements. The results suggest a viable, scalable path toward broader adoption of formal methods by integrating AI-assisted specification generation into typical developer workflows. Future work will broaden pattern catalogs, explore divide-and-conquer strategies for larger codebases, and evaluate smaller, open-source models for cost-performance trade-offs.

Abstract

Recent verification tools aim to make formal verification more accessible to software engineers by automating most of the verification process. However, annotating conventional programs with the formal specification and verification constructs (preconditions, postconditions, loop invariants, auxiliary predicates and functions and proof helpers) required to prove their correctness still demands significant manual effort and expertise. This paper investigates how LLMs can automatically generate such annotations for programs written in Dafny, a verification-aware programming language, starting from conventional code accompanied by natural language specifications (in comments) and test code. In experiments on 110 Dafny programs, a multimodel approach combining Claude Opus 4.5 and GPT-5.2 generated correct annotations for 98.2% of the programs within at most 8 repair iterations, using verifier feedback. A logistic regression analysis shows that proof-helper annotations contribute disproportionately to problem difficulty for current LLMs. Assertions in the test cases served as static oracles to automatically validate the generated pre/postconditions. We also compare generated and manual solutions and present an extension for Visual Studio Code to incorporate automatic generation into the IDE, with encouraging usability feedback.

Figures (11)

• Figure 1: Proposed generate–check–repair-minimize workflow for the automatic generation of specification and verification annotations using LLMs and test oracles.
• Figure 2: Example of a program in Dafny with formal annotations required for successful verification by the Dafny verifier. Our goal is to generate automatically such annotations.
• Figure 3: Examples of common patterns of proof helpers needed in test code.
• Figure 4: Percentage of problems of the TESTDAFNY110 dataset solved after $k$ attempts ($pass@k$) in the direct prompting strategy using different models and configurations.
• Figure 5: Percentage of problems of the TESTDAFNY110 dataset solved after $k$ attempts ($repair@k$) in the repair prompting strategy using different models and configurations.