[derekerdmann]

Static analyzers are NOT formal methods. Reporting no issues just means your tool didn’t find anything, not that your program is correct.

[int0x80]

If a static analyzer is sound, which is something that can be mathematically proven (formal method), will find ALL existing issues plus some false positives if it's not complete (which is almost always the case).

[adrianN]

Formal methods do not necessarily prove the absence of bugs either.

[worik]

> Formal methods do not necessarily prove the absence of bugs either.

They can demonstrate the bugs, when found, are in the specifications

Or in the methods....