研究提出 LLM 辅助 Dafny 形式化验证的十步工作流，在 37 个算法上完成机器检验
研究提出一套面向 Dafny 验证系统的十步 LLM 辅助工作流，覆盖算法形式化、契约开发、不变式经验验证、证明构造、瓶颈分析与资源驱动的证明优化。作者用 Anthropic 的 Claude Opus 5 和 Opus 5.5 在 37 个图论与标记迁移系统算法上实践该流程，并完成了 Hopcroft-Tarjan 三连通性测试的验证，多数机器检验的验证在数小时到数天内完成。
推荐理由：论文给出十步 LLM 辅助 Dafny 验证流程，并在 37 个图论与标记迁移系统算法上实测，可供形式化验证研究者评估迁移。