We introduce HyperDafny, an extension of the well-known verification-aware language Dafny to verify hyperproperties expressed in the temporal logic HyperLTL. HyperDafny generates proof templates whose top-level verification condition is equivalent to the input HyperLTL specification and incorporates program semantics, temporal, and witness obligations. It completes the template by model-guided strengthening, where each failure model reported by Dafny is a counterexample to induction or a witness failure, which HyperDafny excludes by strengthening a relational invariant or a witness relation. We report on the successful verification of 165 instances from three established benchmark suites (30 from HyperQB, 16 from AutoHyper, and 119 from Hypra), covering programs of various sizes and a wide variety of HyperLTL specifications.