Claude stops grinding Dafny proofs one obligation at a time: 37 algorithms machine-checked, triconnectivity test included
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.