Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Inferring multiple helper Dafny assertions with LLMs

Álvaro Silva, Alexandra Mendes, Ruben Martins

TL;DR

This work addresses the barrier of missing helper assertions in Dafny proofs by introducing DAISY, a two-stage system that first localizes where assertions are needed and then infers their content using retrieval-augmented LLM prompts. By extending DafnyBench with w/o-1, w/o-2, and w/o-all datasets and building an assertion taxonomy, the authors provide a rigorous, scalable evaluation framework for multi-assertion inference. The results show that LLM-based fault localization and retrieval-augmented assertion inference can verify a substantial portion of failing programs, with performance improving further when combining localization strategies; multi-assertion cases remain challenging, but many proofs admit multiple valid repair strategies. The work demonstrates meaningful reductions in proof engineering effort and points to promising future directions, including assertion templating, richer context prompts, and ensemble localization strategies to approach oracle-level performance. Overall, DAISY advances automated assistance for formal verification and moves toward more scalable, accessible verification workflows.

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.

Inferring multiple helper Dafny assertions with LLMs

TL;DR

This work addresses the barrier of missing helper assertions in Dafny proofs by introducing DAISY, a two-stage system that first localizes where assertions are needed and then infers their content using retrieval-augmented LLM prompts. By extending DafnyBench with w/o-1, w/o-2, and w/o-all datasets and building an assertion taxonomy, the authors provide a rigorous, scalable evaluation framework for multi-assertion inference. The results show that LLM-based fault localization and retrieval-augmented assertion inference can verify a substantial portion of failing programs, with performance improving further when combining localization strategies; multi-assertion cases remain challenging, but many proofs admit multiple valid repair strategies. The work demonstrates meaningful reductions in proof engineering effort and points to promising future directions, including assertion templating, richer context prompts, and ensemble localization strategies to approach oracle-level performance. Overall, DAISY advances automated assistance for formal verification and moves toward more scalable, accessible verification workflows.

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.

Paper Structure

This paper contains 46 sections, 5 figures, 8 tables.

Table of Contents

  1. Introduction
  2. Contributions:
  3. Motivating Example
  4. Fault Localization:
  5. Assertion Inference:
  6. Methodology
  7. Fault Localization
  8. LLM-based Fault Localization:
  9. Heuristic-based Fault Localization:
  10. Assertion Inference
  11. Multi-embedding for Example Selection:
  12. Inference Strategies:
  13. Assertion Inference Dataset
  14. Assertion Taxonomy:
  15. Evaluation
  16. ...and 31 more sections

Figures (5)

  • Figure 1: Methodology Overview
  • Figure 2: Distribution of the number of valid insertion points for the ground truth assertion.
  • Figure 3: Maximum line distance between valid insertion points for the same ground truth assertion.
  • Figure 4: Fix Position Categorization by LLM for w/o-1
  • Figure 5: Success Rate and localization distribution for w/o-1