# Laurel: Unblocking Automated Verification with Large Language Models

arXiv: https://arxiv.org/abs/2405.16792 · HTML: https://mlsanity.com/paper/2405.16792/

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- Builds on 30 of its 71 references that are in the map.
- First posted on arXiv 27 May 2024.

## Builds on (most cited first, 30 of 30)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Dense Passage Retrieval for Open-Domain Question Answering](https://mlsanity.com/paper/2004.04906/) (2020)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [What Makes Good In-Context Examples for GPT-3?](https://mlsanity.com/paper/2101.06804/) (2021)
- [Fantastically Ordered Prompts and Where to Find Them: Overcoming Few-Shot Prompt Order Sensitivity](https://mlsanity.com/paper/2104.08786/) (2021)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Text and Code Embeddings by Contrastive Pre-Training](https://mlsanity.com/paper/2201.10005/) (2022)
- [code2vec: Learning Distributed Representations of Code](https://mlsanity.com/paper/1803.09473/) (2018)
- [Selective Annotation Makes Language Models Better Few-Shot Learners](https://mlsanity.com/paper/2209.01975/) (2022)
- [Practical Program Repair in the Era of Large Pre-trained Language Models](https://mlsanity.com/paper/2210.14179/) (2022)
- [Keep the Conversation Going: Fixing 162 out of 337 bugs for 0.42 each using ChatGPT](https://mlsanity.com/paper/2304.00385/) (2023)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [An Information-theoretic Approach to Prompt Engineering Without Ground Truth Labels](https://mlsanity.com/paper/2203.11364/) (2022)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [Ranking LLM-Generated Loop Invariants for Program Verification](https://mlsanity.com/paper/2310.09342/) (2023)
- [Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming](https://mlsanity.com/paper/2405.01787/) (2024)
- [A systematic literature review on source code similarity measurement and clone detection: techniques, applications, and challenges](https://mlsanity.com/paper/2306.16171/) (2023)
- [VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search](https://mlsanity.com/paper/2402.08147/) (2024)
- [From Words to Code: Harnessing Data for Program Synthesis from Natural Language](https://mlsanity.com/paper/2305.01598/) (2023)
- [Leveraging Large Language Models to Boost Dafny's Developers Productivity](https://mlsanity.com/paper/2401.00963/) (2024)
- [Using a Nearest-Neighbour, BERT-Based Approach for Scalable Clone Detection](https://mlsanity.com/paper/2309.02182/) (2023)
- [Flux: Liquid Types for Rust](https://mlsanity.com/paper/2207.04034/) (2022)
- [Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny](https://mlsanity.com/paper/2303.00152/) (2023)

## Built on by (most cited first, 11 of 11)

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast](https://mlsanity.com/paper/2411.02318/) (2024)
- [Neural Theorem Proving for Verification Conditions: A Real-World Benchmark](https://mlsanity.com/paper/2601.18944/) (2026)
- [Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction](https://mlsanity.com/paper/2602.04892/) (2026)
- [Certified Program Synthesis with a Multi-Modal Verifier](https://mlsanity.com/paper/2604.16584/) (2026)
- [Automating Formal Verification with Reinforcement Learning and Recursive Inference](https://mlsanity.com/paper/2605.30914/) (2026)
- [Nidus: Externalized Reasoning for AI-Assisted Engineering](https://mlsanity.com/paper/2604.05080/) (2026)
- [Natural Language based Specification and Verification](https://mlsanity.com/paper/2605.11315/) (2026)
- [An Empirical Study of LLM-Generated Specifications for VeriFast](https://mlsanity.com/paper/2606.26490/) (2026)
- [SkillSpec: Intent-Masked Specification Reasoning for Agent Skill Correctness](https://mlsanity.com/paper/2609.06052/) (2026)

## Abstract (arXiv)

Program verifiers such as Dafny automate proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires hints in the form of assertions, creating a burden for the proof engineer. In this paper, we propose Laurel, a tool that alleviates this burden by automatically generating assertions using large language models (LLMs). To improve the success rate of LLMs in this task, we design two domain-specific prompting techniques. First, we help the LLM determine the location of the missing assertion by analyzing the verifier's error message and inserting an assertion placeholder at that location. Second, we provide the LLM with example assertions from the same codebase, which we select based on a new proof similarity metric. We evaluate our techniques on our new benchmark DafnyGym, a dataset of complex lemmas we extracted from three real-world Dafny codebases. Our evaluation shows that Laurel is able to generate over 56.6% of the required assertions given only a few attempts, making LLMs an affordable tool for unblocking program verifiers without human intervention.