What you got here is one thing that make test-case generation tools (quickcheck, fuzzing) still useful even if you've done a full functional (platinum-level) pr

What you got here is one thing that make test-case generation tools (quickcheck, fuzzing) still useful even if you've done a full functional (platinum-level) proof of your program. Functional proof, at least in Spark, doesn't give you hard guarantees about running time, stack or heap space. So even after you've proved the absence of runtime errors in your deserializer, you might still be able to generate a test-case that blows the allowed stack size, or the available heap. Some tools are starting to emerge, like gnatstack for Ada & Spark that gives (or tries to give you) the maximum stack size, statically - a parallel step to compilation, like the Spark examiner and prover). It's very limited in my opinion (some dynamic-sized object returned on the stack are not handled yet, function pointers, I don't have the list handy but it was quite limited). You can get similar stuff (less integrated) with gcc options, IIRC. There's also all the work on WCET that might get interesting but modern architectures are so complex and changing that I'm not sure we'll get near ubiquitous, user-friendly availability for those tools in the near future (next 10 years). For the time being it's mostly used in 'hard' safety-critical projects (avionics), especially since multicore, deeply pipelined architectures, with shared resources (memory, cache, buses) are getting used more and more and they're harder to predict than the previous architectures.