Comment by matthewjheaney

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.