The language combines ideas from the functional and imperative paradigms; it includes support for object-oriented programming.

[2] Dafny was created by Rustan Leino at Microsoft Research after his previous work on developing ESC/Modula-3, ESC/Java, and Spec#.

Dafny was designed as a verification-aware programming language, requiring verification along with code development.

Dafny builds on the Boogie intermediate language which uses the Z3 automated theorem prover for discharging proof obligations.

[9] Methods consist of sequences of statements following a familiar imperative style whilst, in contrast, the body of a function is simply an expression.

The following example illustrates using loops: This fails verification because Dafny cannot establish that (sum + arr[i]) >= 0 holds at the assignment.

Whilst the underlying logic does require such an invariant, Dafny automatically infers this and, hence, it can be omitted at the source level.

Specifically, hiding the contents of a function using the protected modifier can limit what properties can be established about it.