This is a list of notable tools for static program analysis (program analysis is a synonym for code analysis).
(7.8) (6.3.5) Tools that use sound, i.e. over-approximating a rigorous model, formal methods approach to static analysis (e.g., using static program assertions).
Sound methods contain no false negatives for bug-free programs, at least with regards to the idealized mathematical model they are based on (there is no "unconditional" soundness).
Note that there is no guarantee they will report all bugs for buggy programs, they will report at least one.