{
  "annotation_id": "ae284628-aafa-47b4-9c04-4d9c912f5a30",
  "date_created": "2026-02-17T05:53:04.880000Z",
  "date_modified": "2026-02-17T05:53:04.880000Z",
  "file_hash": "2d11b7c6eeca626792bfa97d214df67336f881a302b7013e3b17b32cb6d1e62f",
  "private": false,
  "record": {
    "abstract": "We present DafnyPro, an inference-time framework that enhances LLMs for generating verification annotations in Dafny. DafnyPro comprises three key components: a diff-checker that prevents modifications to base program logic, a pruner that removes unnecessary invariants, and a hint-augmentation system that retrieves and applies predefined, problem-independent proof strategies. We evaluate DafnyPro using Claude Sonnet 3.5 and 3.7 on four benchmarks: Clover, MBPP-Dafny, HumanEval-Dafny, and DafnyBench, achieving consistent performance gains in all cases. Notably, on DafnyBench, the most challenging benchmark, Claude Sonnet 3.5 enhanced with DafnyPro achieves 86% correct proofs, a 16 pp improvement over the base model. We also fine-tune two Qwen models on training data derived from verification attempts by larger models enhanced with DafnyPro. Our 7B and 14B models achieve 68% and 70% correct proofs on DafnyBench, respectively, demonstrating that smaller models can maintain high verification accuracy.",
    "arxiv_id": "2601.05385",
    "authors": [
      "Debangshu Banerjee",
      "Olivier Bouissou",
      "Stefan Zetzsche"
    ],
    "categories": [
      "cs.SE"
    ],
    "license": "http://arxiv.org/licenses/nonexclusive-distrib/1.0/",
    "title": "DafnyPro: LLM-Assisted Automated Verification for Dafny Programs",
    "url": "https://arxiv.org/abs/2601.05385",
    "version": "v1"
  },
  "schema_id": "dorsal/arxiv",
  "source": {
    "execution_id": "f0c502ed-14ad-48e7-a663-401d5b31f6e6",
    "id": "arXiv Dataset",
    "type": "Model",
    "variant": "snapshot-2026-01-17",
    "version": "0.1.0"
  },
  "user_id": 1000002
}