DafnyBench: A Benchmark for Formal Software Verification

TL;DR

DafnyBench is a large benchmark designed to evaluate machine learning models' ability to assist formal software verification, demonstrating that LLMs can verify over 750 programs with a 68% success rate using hints and feedback.

Contribution

This paper introduces DafnyBench, the largest benchmark for training and evaluating ML systems in formal software verification, and assesses LLMs' effectiveness in generating hints for verification.

Findings

LLMs can verify over 750 programs with a 68% success rate.

Feedback from error messages improves verification success.

Verification success decreases as code complexity and hint requirements increase.

Abstract

We introduce DafnyBench, the largest benchmark of its kind for training and evaluating machine learning systems for formal software verification. We test the ability of LLMs such as GPT-4 and Claude 3 to auto-generate enough hints for the Dafny formal verification engine to successfully verify over 750 programs with about 53,000 lines of code. The best model and prompting scheme achieved 68% success rate, and we quantify how this rate improves when retrying with error message feedback and how it deteriorates with the amount of required code and hints. We hope that DafnyBench will enable rapid improvements from this baseline as LLMs and verification techniques grow in quality.