Dafny enables automated verification of heap-manipulating programs using an SMT solver, allowing verification of large, realistic codebases. However, when proofs require manual effort, the automation comes at the price of visibility into proof states, which can be challenging in the case of programs with non-local control flow. This paper presents a methodology for dealing with such programs using Lean, an interactive theorem prover. We extract straight-line programs for execution paths, embed a fragment of Dafny’s semantics into Lean, and provide a verified weakest-precondition generator. We argue for the use of Lean’s semi-manual interactive proving when dealing with difficult Dafny proofs.