With this new version of the SPARK Pro toolset, AdaCore comes one step closer to its goal of making the writing of proven software both efficient and pleasant. As part of its new SPARK Pro 16 integrated development and verification environment, AdaCore further simplifies software engineers' transition to greater reliance on static verification and formal proofs sans need for expertise in mathematical logic. SPARK Pro 16 also provides enhanced coverage of the SPARK 2014 language features and now supports the Ravenscar tasking profile, thus extending the benefits of formal verification methods to a safe subset of Ada 2012 concurrent programming features. This new SPARK Pro can generate counter-examples to verification conditions that cannot be proved, making it easier for developers to find defects in the functional code or in the supplied contracts. Finally, SPARK Pro 16 also improves the handling of bitwise/modular operations, and the product's proof engine now includes the Z3 SMT solver.