[nickpsecurity]

One of the things I like about this article is that it gives another example showing how formal methods catches deep errors unlikely to be caught with human review or testing:

"Overall, the error trace found by Infer has 61 steps, and the source of null, the call to X509 _ gmtime _ adj () goes five procedures deep and it eventually encounters a return of null at call-depth 4. "

I think the example Amazon gave for TLA+ was thirty-something steps. Most people's minds simply can't track 61 steps into software. Tests always have a coverage issue.