Dafny-Annotator: AI-Assisted Verification of Dafny Programs

This conference talk explores the development of dafny-annotator, a tool that uses Large Language Models and search techniques to automatically add logical annotations to Dafny programs until they can be formally verified. Learn how researchers from Stanford and Harvard Universities addressed the challenge of formal verification adoption by creating AI assistance for Dafny users. Discover their approach combining LLaMa 3.1 models with search strategies, which initially achieved only 15.7% success on DafnyBench test methods. Follow their innovative solution to the limited training data problem through the creation of DafnySynth, a synthetic dataset generated by having LLMs formulate ideas, implement them, and propose incremental changes validated by Dafny. See how fine-tuning on both datasets significantly improved success rates to 50.6%, demonstrating a promising path toward AI assistants for programming languages with limited human-generated examples, potentially reducing barriers to formal verification adoption.