Clover
Closed-Loop Verifiable Code Generation
Checks mutual consistency between code, docstrings, and formal Dafny specifications using SMT equivalence and deductive verification.
The loop
- Proposes
An LLM generates Dafny implementation code, formal preconditions/postconditions, and loop invariants from a problem description.
- Judged by
The Dafny/Boogie/Z3 verifier checks that the code satisfies the specification and tests logical equivalence between reconstructed specs and test suites.
- Steers
Z3 verification errors and equivalence counterexamples are returned to the LLM to repair either the implementation or the annotations.
Headline result
Accepted 87% of correct Dafny programs while rejecting all of adversarial incorrect synthesis candidates on the CloverBench suite.
What this does not prove
Of the six checks, the Dafny verifier checks the code against its annotations and five reconstruction tests each use an LLM.
How it generalizes the harness
The Dafny/Z3 SMT verifier checks deductive correctness and specification equivalence across the synthesis loop.
Classification
| What it proposes | Program |
|---|---|
| Generative model | GPT-4 Dafny code and specification generator |
| Algorithmic authority | Dafny compiler and Z3 SMT solver |
| Feedback | Verifier errors |
| What gets updated | Prompt context |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Code released |
| Lineage | Original system |