I have found huge value in CBMC and KLEE for statically verifying C code for real time safety critical embedded applications.

ACL2 is also VERY powerful and capable.