State-of-the-art binary code analysis tools

There is no such thing as a bug free software. Today I stumbled on this:
This is an unfortunate and sad truth about programming: regardless of our efforts, software will have bugs; it will crash, it will burn, it will fail. At the same time there is a hope:
We desperately need code verification tools like this.