By the way, if you want to know more and dive in, we just completed a 3-days training sessions with AdaCore's Yannick Moy and all the colleagues (some not even Ada practitioners) are itching to put some SPARK everywhere, and were surprised the tech is so accessible, mature, for non-formal-praxis people. We're probably going to book a second session for mostly C dev people.
Give it a try!
(I have no stakes there, but wanting devs to focus on safety, security and better software - more direct value in our daily work)