arXiv cs.AI· Wieger Wesselink, Kees Huizing, Huub van de Wetering·· 1 天前AI 评分38
用 Claude Opus 5 辅助 Dafny 形式化验证：十步工作流覆盖 37 个算法
LLM-Assisted Verification in Dafny
AI 导读
一项研究提出基于 Dafny 验证系统的十步 LLM 辅助工作流，用 Anthropic 的 Claude Opus 5 与 Opus 5.5 完成算法形式化、契约开发、不变量验证、证明构建与性能优化。在 37 个图论与标记迁移系统算法上完成机器校验验证，其中包括 Hopcroft-Tarjan 三连通性测试，多数验证在数小时至数天内完成。人类验证者的角色由此转向规范审查与策略指导。
正文 · 原文
Abstract:Formal verification of complex algorithms requires expertise in program specification, invariant construction, mathematical proof, and the management of automated theorem provers. Although large language models (LLMs) can generate program code and proof fragments, reliably developing complete machine-checked verifications remains challenging: it requires an iterative process of constructing and validating specifications and invariants, building proofs, diagnosing solver failures, and optimizing verification performance. This paper presents a systematic ten-step workflow for LLM-assisted verification of scientific algorithms using the Dafny verification system. The workflow integrates algorithm formalization, contract development, empirical invariant validation, proof construction, bottleneck profiling, and resource-driven proof optimization. We applied the workflow using Antrhopic's Claude Opus 5 and Opus 5.5 models, combining LLM-driven development with automated testing and verification feedback, while retaining human oversight for correctness-critical decisions and strategic interventions. We evaluate the approach on 37 complex algorithms from graph theory and labelled transition systems. Notably, we verified the Hopfcroft-Tarjan triconnectivity test, demonstrating that even highly challenging algorithmic verification tasks can be carried out through a structured LLM-assisted workflow. Many of our machine-checked verifications were obtained within hours to a few days of interactive development. Our results suggest that LLM-assisted workflows can shift the role of the human verifier from detailed proof construction toward supervision, specification review, and strategic guidance.
| Comments: | 16 pages (excluding references), 20 pages including references; 1 figure, 2 tables. Submitted to FSEN 2027 |
| Subjects: | Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Software Engineering (cs.SE) |
| MSC classes: | 68N30, 68Q60, 68V15 |
| ACM classes: | D.2.4; I.2.2; F.3.1 |
| Cite as: | arXiv:2611.16886 [cs.LO] |
| (or arXiv:2611.16886v1 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2611.16886 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Wieger Wesselink [view email]
[v1]
Thu, 12 Nov 2026 14:48:38 UTC (51 KB)
来源：arXiv cs.AI · arxiv.org