DafnyBench v1：程序证明注解补全
原作者以现有Dafny程序移除提示，再让模型补全并验证。
原文位置：Benchmark construction / evaluation；官方sun-wendy/DafnyBench
不能据此推出：受限程序/固定规格，不等于自动发现业务规格或验证整个生产系统；历史模型不代表今天。
核查 2026-10-20 · 所属资料版本 2026-10-21.workunits.2 · 来源ID WU-M-DAFNY
实际引用在哪里
程序与系统验证：规格、反例和证明产物相互对照 →
固定规格下的程序验证注解任务证据。
关系：部分支持