Those are all actually the same proof. The proofs that the analysis provides about the program are essentially the soundness proof of the analysis combined with

Those are all actually the same proof. The proofs that the analysis provides about the program are essentially the soundness proof of the analysis combined with its output. So if I prove that the signs that values of a variable can hold will be contained in the set found by my static analysis, and my analyzer outputs {+}, then that is a proof that that variable can only store positive values. It produces a proof in the same sense that, if I prove the Pythagorean theorem, then I can evaluate the expression sqrt(x^2+y^2) with x=3 and y=4 to get a proof that the corresponding line has length 5. Getting an incorrect proof out of that would be tantamount to an arithmetic error. Note that most analyses do no actual automated theorem proving; they just, conceptually at least, instantiate existing proofs. If, by "find a proof," you mean "show the presence of bugs if there are any," then that's part of the same soundness proof. Conversely, showing the absence of bugs if there aren't any is completeness; you can't have both due to the halting problem. Whether an analyzer correctly implements an analysis is a totally separate beast, and is an example of verification. Xavier Leroy has done some excellent work in verifying static analyzers.