Laurel: Unblocking Automated Verification with Large Language Models

This conference talk presents "Laurel," a tool that uses large language models (LLMs) to automatically generate assertions for program verification in Dafny. Learn how researchers from the University of California San Diego developed domain-specific prompting techniques to help LLMs determine assertion locations and generate appropriate hints for SMT solvers. Discover how Laurel analyzes verifier error messages to insert assertion placeholders and leverages a new proof similarity metric to select relevant example assertions from the same codebase. The presentation shares evaluation results from the DafnyGym benchmark, demonstrating that Laurel successfully generates over 56.6% of required assertions within a few attempts, effectively reducing the burden on proof engineers and enabling automated verification without human intervention. The 18-minute talk was delivered at the Dafny 2025 workshop on January 19, 2025, sponsored by ACM SIGPLAN.