My colleagues Claire Dross and Martyn Pike have put together a course in five lessons to introduce the various analyzes performed on SPARK code. This course was just made available on AdaCore University. I have already used it twice in trainings for customers and partners, and I've received extremely good feedback on the quality of the slides. With Martyn's warm and vibrant voice in the online version, that's even better! Definitely a must-see if you want to have a tour of the technology.