The paper introduces Diversify2Verify, a staged LLM-based pipeline for Why3 that generates diverse recursive and imperative array/list implementations to enhance automated verifiability. The approach infers representation-specific contracts and employs bounded verifier-guided annotation repair to handle verification failures.
- The authors constructed a benchmark of 73 tasks over integers, arrays, and lists, yielding 292 implementation variants.
- Diversify2Verify initially verified 96 artifacts, increasing to 154 after two repair passes.
- Artifact-level verification improved from 32.9% to 52.7%.
- At the task level, at least one variant verified for 49 of 73 tasks, achieving a 67.1% success rate.
These results demonstrate that implementation diversity helps find verification-friendly artifacts among task-equivalent programs.