David Mentré from Mitsubishi Electric R&D Centre Europe has produced a very interesting report on his use of GNATprove (the formal verification tool we develop for the next version of SPARK) on a case-study from the Open-ETCS European project, to develop the tools for the future European Train Control Systems.
Although David asked me to mention this is highly experimental (neither fully proved nor fully tested), I think it shows quite well what one can do with formal verification. The report contains inlined code showing how some units were specified using preconditions/postconditions and annotated with assertions for proofs. You can also download the code from github, or browse it online.
David will present this model at an internal Open-ETCS meeting next Monday, I’ll ask him to post the conclusion of his presentation!