Claude stops grinding Dafny proofs one obligation at a time: 37 algorithms machine-checked, triconnectivity test included
Synopsis
A team at Eindhoven University of Technology organized LLM-assisted Dafny verification into a ten-step workflow in which Claude Code acts as a verification construction agent, producing specifications, implementations, invariants and proofs under human supervision. The workflow yielded machine-checked Dafny implementations for 37 algorithms from graph theory, labelled transition systems and computational geometry, including the Hopcroft–Tarjan triconnectivity test; the authors report many verifications within hours to a few days, but ran no controlled comparison against human-led verification.
Interpretation
The bottleneck in formal verification shifts from writing the mathematical argument to making the proof checker able to handle the proof, and a large language model is placed inside a fixed-step, human-gated process to carry that engineering work. Earlier LLM work on Dafny concentrated on single tasks such as lemma generation, annotation synthesis or loop-invariant generation, or assumed an existing implementation and supplied missing proofs. The workflow covers the full development path from a literature algorithm description through specification, implementation, invariants, proofs and verification optimization, and produced machine-checked Dafny implementations for 37 algorithms.
The workflow splits verification into a specification phase, a code-generation and contract-testing phase, and a proof-development phase, each with defined inputs, outputs and completion criteria. In the specification phase the agent transcribes the published algorithm into pseudocode and formalizes its intended behavior as pre- and postconditions, which a human reviews and locks so it cannot change without explicit approval. In the proof phase the agent first verifies each proof obligation in isolation inside resource-restricted subagent loops, then iterates until the whole file verifies under Dafny's native configuration, and audits the result for unjustified assumptions.
Solver resource measurements are used to guide proof restructuring, not merely to decide whether a proof passes. The main verification routine of the Lengauer–Tarjan dominator algorithm originally had 644 proof obligations with 36 timeouts and about 2.1 billion Z3 resource units. After hiding contracts and invariants behind opaque predicates and revealing facts only through explicit lemmas, the obligation count fell to 271, all timeouts were eliminated, and resource consumption dropped to 144 million units.
Perspective
The demonstrated scope is published algorithms given as pseudocode, covering 37 targets from graph theory, labelled transition systems and computational geometry, verified with Dafny 4.10.0 and its bundled Z3 under a six-core, 12 GB memory limit per run; low-level implementation details, memory management and language-specific optimizations are out of scope.
The authors note that the selected algorithms are well known and likely represented in the training data of contemporary LLMs, with the extent of that representation unknown; performance on unpublished or previously unseen algorithms, or on existing source code rather than paper descriptions, is not established; no controlled comparison with human-led verification was performed, and the contribution of individual workflow components was not isolated; correctness claims remain conditional on the accuracy of the human-reviewed specification and on the soundness of Dafny and its underlying solver.