TLDR: A new tool called DAISY uses Large Language Models (LLMs) and a hybrid fault localization method to automatically infer missing helper assertions in Dafny programs. It successfully verifies 63.4% of programs with one missing assertion and 31.7% with multiple, significantly reducing manual proof engineering effort and making formal verification more accessible.
Formal verification tools like Dafny are powerful for ensuring software correctness, but they often demand a lot of manual effort. Developers frequently need to add “helper assertions” – extra statements that guide the verifier without changing how the program behaves. Identifying and placing these assertions is a significant challenge, often consuming a large portion of the proof engineering time. This manual burden is a major reason why formal methods aren’t more widely adopted.
A new research paper, “Inferring multiple helper Dafny assertions with LLMs,” by Álvaro Silva, Alexandra Mendes, and Ruben Martins, explores how Large Language Models (LLMs) can automate this process. Their work focuses particularly on scenarios where multiple helper assertions are missing, which is a common and complex problem in verification.
DAISY: A New Approach to Assertion Inference
The researchers developed a new tool called DAISY (Dafny Assertion Inference SYstem). DAISY tackles the problem in two main stages: fault localization and assertion inference. Fault localization identifies where the missing assertions should be placed, and assertion inference then generates the actual content of these assertions.
For fault localization, DAISY uses a hybrid method. It combines predictions from an LLM with heuristics derived from the verifier’s error messages. This dual approach has proven more effective than using either method alone. The LLM-based localization can even suggest multiple positions for assertions, which is crucial for programs requiring more than one fix.
Once the locations are identified, the assertion inference stage uses an LLM to generate candidate assertions. The system can generate up to ten potential assertions for each identified location. To improve the quality of these generated assertions, DAISY employs a technique called Retrieval-Augmented Generation (RAG). This involves finding similar, already verified code examples and their corresponding assertions to provide the LLM with relevant context.
Performance and Key Findings
The team evaluated DAISY on an extended version of the DafnyBench benchmark, which includes programs with one, two, or even all assertions removed. The results are promising:
- For programs with one missing assertion, DAISY successfully verified 63.4% of them.
- For programs with multiple missing assertions, DAISY achieved a 31.7% verification success rate.
A notable finding is that many programs can be verified with fewer assertions than originally present. This highlights that there can be multiple valid ways to prove a program’s correctness, and it’s not always necessary to recover every original assertion. The combination of LLM-based and heuristic-based fault localization proved to be highly complementary, significantly boosting overall performance.
The researchers also categorized assertions into types (INDEX, TEST, MULTI, OTHER) to understand inference difficulty. They found that “TEST” assertions (those resembling unit tests) were generally the easiest to infer, while “MULTI” assertions (spanning multiple lines) were the most challenging. This insight suggests that a two-stage workflow could be effective: first, an LLM generates test-like specifications, and then a second LLM infers helper assertions to satisfy these conditions.
Also Read:
- HAFixAgent: Leveraging Repository History for Smarter Software Bug Repair
- Decoding Code Agent Decisions: An Analysis of Success and Failure Paths
Future Directions and Impact
While DAISY shows significant progress, the paper also discusses areas for improvement. Challenges remain with complex multi-line assertions, intricate indexing and sequence reasoning, and cases where the LLM lacks sufficient context about auxiliary functions or lemmas. Future work could involve integrating assertion templates, enriching prompts with more contextual definitions, and refining ensemble strategies.
This research represents a crucial step towards making formal verification more scalable and accessible. By automating the inference of helper assertions, DAISY can substantially reduce the manual effort involved in proof engineering, allowing developers to leverage the strong correctness guarantees of tools like Dafny more easily. For more details, you can read the full research paper here.
