"I forgot to ask an obvious question: Dafny uses .Net's garbage collection, right? If so, that presumably rules out its use on hard real-time systems."
I was just about to point that out. Yes, Dafny uses garbage collection (which makes formal verification much easier). As far as I know in SPARK (and FRAMA-C), verification of memory allocation is still an open research question.
I was just about to point that out. Yes, Dafny uses garbage collection (which makes formal verification much easier). As far as I know in SPARK (and FRAMA-C), verification of memory allocation is still an open research question.