The problem with Ada is not only the lack of tooling (although it's a huge problem - relatively to C, the tooling is scarce and horrible), it's also the people that know the language. I prefer C code written by a good programmer than Ada code written by a poor programmer any day, and finding good C programmers is much easier than finding good Ada programmers.

Detailed account of using Spark and PVS theorem prover in such an app

http://www.cs.virginia.edu/~jck/publications/Xiang.Yin.disse...

And more people who can write it or prefer writing in it? Technical problems being people problems 90% of the time or whatever it was the fella said.