用 LLM 辅助 Dafny 形式化验证：系统性十步工作流
LLM-Assisted Verification in Dafny
AI 导读
一篇 arXiv 论文提出基于 Dafny 验证系统的 LLM 辅助形式化验证十步工作流，涵盖算法形式化、契约开发、不变式验证、证明构建与性能优化。
正文 · 原文
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