If you're somewhat interested in formal methods applied to software, but you never had the chance to really look at it, now is the time! Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College have written a truly essential book for getting up to speed with formal verification using SPARK. I really love this book, and here are the aspects I love most:

• It does not assume you know static analysis. It does not assume you know logic. It does not assume you know Ada. Instead, it introduces all the concepts that are useful for using SPARK where needed, with a clarity and simplicity of exposure that is remarkable.
• It was written by very experienced users and teachers of the technology, but not by the tool builders (us at AdaCore and Altran). So they focus on the application of the technology in software engineering (in the problem domain) rather than on the technology prowesses (in the solution domain), which is a typical bias for tool builders writing on their technology.
• It is very practical, full of examples that illustrate all the concepts they explain and the tips they give on the actual practice of an engineer applying formal verification with SPARK on her code.

I see this book as a glorified User's Guide to SPARK, and I recommend it to anybody who either wants to have a first look at SPARK, or actually starts using it for real. In fact, we also try to apply the principles above in the SPARK User's Guide, but their book is definitely a better entry door to the technology, while the User's Guide tries to be its map. Besides the publisher's webpage, you can find it on Amazon and many other online bookstores.

For those in academia who would like to teach SPARK, the book is ideally structured with a summary and exercises closing each chapter. All examples are available from the publisher's webpage (see Resources and Source code) and the final case study on a time stamp server is available from one of the authors's github. You may also get a free copy of the book from Cambridge University Press to evaluate it for your course (see the publisher's webpage).