DafnyFix: Single-Transformation Automated Repair in Dafny

Abstract

Formal verification using verification-aware languages, like Dafny, ensures a program’s conformance to its specification. Assuming a correct and complete specification, a verification failure may indicate an implementation fault that the developer must identify and correct. However, debugging verification failures is particularly challenging, as verification diagnostics do not directly hint at the implementation changes required for verification to succeed. Automated Program Repair has long been explored for traditional programming languages to reduce manual debugging effort, yet it remains largely underexplored in verification-aware contexts.
We propose DafnyFix, a repair framework for Dafny that searches over a space of single-transformation candidate patches generated through three complementary heuristics: existing mutation testing operators, newly introduced repair-oriented mutation operators, and state-guided repair templates inspired by AutoFix. We evaluate DafnyFix’s effectiveness on a dataset of implementation faults in LLM-generated Dafny programs curated from the dafny-synthesis benchmark, and successfully repair 62.5% of the faults, showing that small deterministic transformations can repair a substantial number of faulty LLM-generated implementations. Our results further show that the proposed repair heuristics are complementary, targeting different categories of implementation faults. Additionally, we identify six fault patterns of LLM-generated programs in our dataset that can be corrected by small program transformations.

Alexandra Mendes

Assistant Professor

My research focuses on encouraging a wider adoption of software verification by creating tools and methods that hide the complexities of verifying software. Much of my most recent work overlaps with the area of software engineering. For more details, see selected publications and some of my projects. Follow me on Twitter or add me on LinkedIn. See also the Software Reliability Lab website.