Oh, yes, that's what the SPARK language does. There's also CodePeer, which does a static analysis of your Ada code. GNAT itself also does many static checks.
Oh please, the comparison of Ada to COBOL is invidious. Ada simply requires you to be explicit about your intent. This is a feature, not a flaw. You mean to say that you've never been burned by an implicit conversion in C, or a misplaced semi-colon? Ada is no less verbose than Java.
Right. Also note that GNAT is just GCC. The most recent language standard is Ada 2012. (I was involved in the design of the Ada standard container library, which originally appeared in Ada 2005.)
Right, VHDL designed by the team at Intermetrics (which has also had a long association with Ada -- Ben Brosgol was the designer of the Red language that lost out to Green).