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

TL;DR

This paper demonstrates how large language models can automatically generate formal verification annotations for Dafny programs from natural language comments and test code, significantly reducing manual effort.

Contribution

It introduces a multimodel LLM approach that automates the creation of formal specifications and proof helpers in Dafny, achieving high accuracy with minimal iterations.

Findings

Correct annotations generated for 98.2% of programs

Test assertions effectively validate generated specifications

Proof-helper annotations are key to problem difficulty

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.