Inferring multiple helper Dafny assertions with LLMs

TL;DR

This paper presents DAISY, a tool using LLMs to automatically infer missing helper assertions in Dafny programs, significantly reducing manual effort and improving verification scalability.

Contribution

The paper introduces a novel hybrid approach combining LLMs and heuristics for inferring multiple missing assertions in Dafny, supported by a new benchmark and taxonomy.

Findings

DAISY verifies 63.4% of single-assertion cases

DAISY verifies 31.7% of multiple-assertion cases

Many proofs can be completed with fewer assertions than originally provided

Abstract

The Dafny verifier provides strong correctness guarantees but often requires numerous manual helper assertions, creating a significant barrier to adoption. We investigate the use of Large Language Models (LLMs) to automatically infer missing helper assertions in Dafny programs, with a primary focus on cases involving multiple missing assertions. To support this study, we extend the DafnyBench benchmark with curated datasets where one, two, or all assertions are removed, and we introduce a taxonomy of assertion types to analyze inference difficulty. Our approach refines fault localization through a hybrid method that combines LLM predictions with error-message heuristics. We implement this approach in a new tool called DAISY (Dafny Assertion Inference SYstem). While our focus is on multiple missing assertions, we also evaluate DAISY on single-assertion cases. DAISY verifies 63.4% of programs with one missing assertion and 31.7% with multiple missing assertions. Notably, many programs can be verified with fewer assertions than originally present, highlighting that proofs often admit multiple valid repair strategies and that recovering every original assertion is unnecessary. These results demonstrate that automated assertion inference can substantially reduce proof engineering effort and represent a step toward more scalable and accessible formal verification.