I am very pleased to announce that a book is now available for those who want to learn formal verification with SPARK 2014. This book was written by Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College. We've been interacting a lot with them since they started in 2013, and the result of these interactions is quite satisfying! Here is my review on AdaCore's blog.
All the examples presented in the book and the Thumper case study presented in chapter 8 are available as examples in the development version of the SPARK toolset. That gives an easy way to practice while reading the book: just open GPS, and select the spark_book or thumper example in menu Help-->SPARK-->Examples. There is also a brief description of both examples in the SPARK UG.