Have you tried SPARK Ada? It was first to be designed to automate proofs of common attributes such as immunity to lots of code injections or crashes that happen in C. They have both automated and interactive proving for other conditions you put in as preconditions, invariants, and postconditions. Need more people building reusable specs and code in such languages. Others from Microsoft are VCC compiler and Dafny language. From CompSci, Frama-C and Jave Modeling Language.