I found a good summary on StackOverflow: "Dafny is based on a Java or C# like imperative language with the ability to write Hoare logic style state invariants,

I found a good summary on StackOverflow: "Dafny is based on a Java or C# like imperative language with the ability to write Hoare logic style state invariants, this allows users of the languages to verify properties about methods, and objects that use mutable state, loops, arrays, and so on. Dafny's core theory is a custom program logic mostly designed by Rustan and a handful of collaborators. Dafny discharges the verification conditions it generates by compiling them to Boogie an intermediate verification language, which in turn compiles them into queries which are passed to an SMT solver such as Z3 or CVC4 to discharge." - jroesch