DafnyBench Verifier Repair
Iterative synthesis of loop invariants and helper assertions in Dafny guided by Dafny verifier error messages.
The loop
- Proposes
An LLM inserts loop invariants and assertions into a Dafny program while keeping the top-level specification intact.
- Judged by
The Dafny verifier checks whether the program verifies and returns its error message when it does not.
- Steers
The Dafny error message is fed back for up to 10 attempts until the verifier accepts the proof.
Headline result
Verified 68% of the 782 ground-truth formal verification programs in DafnyBench via multi-turn compiler feedback.
What this does not prove
A spec check must prevent the model from trivially satisfying the verifier by weakening `ensures` clauses or adding `assume false`.
How it generalizes the harness
The Dafny deductive verifier enforces formal proof obligations across iterative invariant synthesis.
Classification
| What it proposes | Proof |
|---|---|
| Generative model | Claude 3 Opus / GPT-4o invariant synthesizer |
| Algorithmic authority | Dafny formal verifier |
| Feedback | Verifier errors |
| What gets updated | Prompt context |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Code released |
| Lineage | Original system |