Dafny Power User is a series of notes with tips about advanced features, explanations and comparisons of related constructs, and general thoughts about the Dafny language. Each note assumes that you have some basic familiarity with Dafny. The notes can be read in any order.
 Calling Lemmas Automatically
 Statement versus Expression Syntax
 Comprehensions
 ShortCircuit Operators
 Automatic Induction
 TypeParameter Completion
 old and unchanged
 Functions over Set Elements
 Iterating over a Collection
 Different Styles of Proofs
 Case study of definitions, proofs, algorithm correctness: GCD
 Typeparameter modes: variance and cardinality preservation
 The Parent Trick for proving termination, and a functionbymethod use case
 Working with coinduction, extreme predicates, and ordinals
 How to choose your number types
Here are some publications that give information, tutorials, or advanced coverage of some Dafny features:

Modular Verification Scopes via Export Sets and Translucent Exports
(K. Rustan M. Leino and Daniel Matichuk; ARND 2018, © Springer)
This paper describes the module system, export sets, and imports. 
Verified Calculations
(K. Rustan M. Leino and Nadia Polikarpova; VSTTE 2013, © Springer)
This paper introduces thecalc
statement, which is the primary construct for writing your own proofs in Dafny. 
Modeling Concurrency in Dafny
(K. Rustan M. Leino; SETSS 2017, © Springer)
Dafny does not support concurrency, but you can model the execution of concurrent programs and protocols. As this tutorial paper describes, this modeling is done in a style akin to that of TLA+, UNITY, EventB, or action systems. 
Using Dafny, an Automatic Program Verifier
(Luke Herbert, K. Rustan M. Leino, and Jose Quaresma; LASER 2011, © Springer)
If you’re working with mutable, dynamically allocated storage in Dafny, you need to know about abstraction and dynamic frames. One account of these is given in sections 8 and 9 of this tutorial. 
Automating Theorem Proving with SMT
(K. Rustan M. Leino; ITP 2013, © Springer)
When you specify and verify more difficult programs in Dafny, you need functions and proofs. This is also true if you want to use Dafny as an interactive proof assistant to write formal models and prove theorems. This paper contains some simple examples of functions, induction, and (advanced!) coinduction. (Note, in current Dafny syntax,ghost method
is calledlemma
andcomethod
is calledcolemma
.) 
Automatic verification of Dafny programs with traits
(Reza Ahmadi, K. Rustan M. Leino, and Jyrki Nummenmaa; FTfJP 2015, © ACM)
Traits are abstract superclasses, variations of which go by various names like interfaces or mixins. This paper describes simple traits in Dafny. Since this paper was written, traits have been expanded and traits can now take type parameters and extend other traits. 
Wellfounded Functions and Extreme Predicates in Dafny: A Tutorial
(K. Rustan M. Leino; IWIL2015, © EPiC)
Describes Dafny’sinductive predicate
andcopredicate
declarations, along withinductive lemma
andcolemma
. These are advanced features and not just simply a recursive predicate or lemma. Note, the publication talks about a restriction to continuous functors. Since the publication, this restriction has been removed in Dafny. This is achieved by changing the type of the indexk
in the paper (see its equations (11) and (12)) fromnat
toORDINAL
. If you really want the previousnat
, Dafny offers some syntax for doing so for each (co)inductive predicate (see the Dafny test suite for examples). 
Programming Language Features for Refinement
(Jason Koenig and K. Rustan M. Leino; REFINE 2015, © EPTCS)
This paper describes Dafny’s refinement modules. These are advanced features aimed at letting you write programs in stages, where each stage introduces more details. However, as the paper reports, these features are not as easy to use as one would like. So, if you’re just looking for a way to separate a module’s implementation from its interface, then it is instead the paper “Modular Verification Scopes via Export Sets and Translucent Exports” above that you want to read. 
Compiling Hilbert’s epsilon operator
(K. Rustan M. Leino; LPAR20, © EPiC)
This paper goes through design considerations of the:
(“assign such that” or “let such that”) operator in Dafny. For a more direct example, see the Dafny Power User note Functions over a set above.