And, even if you don't go 'full platinum level proof' (proof of all the High-Level specs of your software) in SPARK you can still enjoy, without too much effort

And, even if you don't go 'full platinum level proof' (proof of all the High-Level specs of your software) in SPARK you can still enjoy, without too much effort: - proof of no read access to uninitialized variables - proof of absence of runtime errors (overflow, underflow, array out of bound, incorrect conversion...) - proof of type predicates/invariants, asserts, pre/post conditions... - Less known, you can specify and verify 'data provenance' with 'this function's result depends on parameters a and b c' aspects, and you can also specify and verify global variables access (global_in, global_out). This with a language that supports tasking, generics, and oop natively... And proof on access types (pointers) are on the way. Really amazing tech to work with.