SPARK is a technology for mathematically proving that programs are correct, that has completed its 30th birthday in 2017, making it one of the oldest such technology alive! Its longevity can be explained by a stubborn focus on the development of tools usable by software engineers and applicable to industrial software. The "tools" include here a programming language, development and verification tools, and processes around these. These tools have evolved considerably in three decades, with even a complete overhaul between 2010 and 2014 to unify the logical and executable views of specifications. We are seeing now adoption progressing at a faster rate, mostly because the level of automation has decreased entry costs for users. Normal engineers can start proving the correctness of their programs on their personal computers. An apparent paradox is that program proving itself, understood as the full functional correctness of programs, is not much easier today. What is much easier thanks to automation however is the proof of simpler yet critical properties of programs, like the absence of runtime errors. An unavoidable consequence is that, as engineers try to prove more complex properties on their programs, automation is not the panacea. We tell them: Don't Panic! SPARK offers a continuum from automatic proof to interactive proof, allowing users to decide where to set the target of their journey. In this talk, we will provide the hitchhiker's guide to the SPARK proof galaxy.