Without going to full functional proof in Spark (for example) you can go easily as a first step for proof of data flow peoperties ('ooops this buffer size varia

Without going to full functional proof in Spark (for example) you can go easily as a first step for proof of data flow peoperties ('ooops this buffer size variable is not initialized in this strange corner case'), and then without too much effort (compared to exhaustively testing) proof of absence of runtime error (aka this code won't crash). Of course as GP remarks, you'll have explicited all your preconditions and invariants (types or contracts). But that's a choice : either treat the damned corner cases in your code or expose them to your user ("this can't work on input buffers that aren't power-of-2"). If you don't treat the corner case, instead of putting it in the docs, or in the header comments, or asserting right when you start, add it as a precondition or type invariant/predicate. You then get all the power of automated proof tools (please use all my cycles and RAM but prove this) to prove that without the corner case you won't crash and your users get to check (by proof, static analysis, testing, fuzzing, 'careful code reading'...) that they never call your API the wrong way - if they want. I think Frama-C & Spark should sell a bit more the AoRTE stuff. If at least your software won't crash or use uninitialized variables, you'll sleep better. The world would probably be a better place if things like x509, asn1 decoding code and all kinds of file format parsers were proved for 'just' the absence of runtime error... The thing that is nice with most modern formal verification tools is that they're not all-or-nothing propositions. Suppose you already have some Spark code that you've checked (proof) for AoRTE, but didn't go for full proof of all the functional properties of your software (you went for pure-testing with a pinch of static analysis and some code review on critique stuff). You're already high on the correctness scale... You get a report from a customer or security researcher or code auditor that there is a strange behaviour in your code. They can't nail the reason but sometimes you send inconsistent data. No crash or memory corruption, just an output that seems impossible to you (even after full code review and exhaustive test) and out of spec anyways. No reproducer, no idea what was sent to your system, just 'please stop sending us inconsistent data'. One way to find the bug is to try to prove it's not there. Add a post-condition 'fields a and b and c should never be 0 at the same time' and use the tools. Maybe start with structured testing following the code yourself... Then go for unsound static analysis or fuzz testing. Then once you've ran 2 weeks of afl and hongfuzz and didn't trigger this post- and once you've exhausted all the codepeer (or PVS studio or Coverity) false positives and still they didn't find the code path to your bug, and you still need to find this bug, you can use the proof tools and be sure you'll get an answer (after some work) on this specific question. 2 big caveats (for Spark at least) : you'll have to restrict yourself to the Spark subset of Ada (mostly, no pointers, no aliasing - but this subset is deemed to grow once the proof tools improve...) and second : automated proof with floating point numbers is not there yet and it is a hard research topic.