[rurban]

Not fun, a serious tool, and extremely easy to use, unlike other formal methods. It works with your source code, not on some rewritten abstraction of it.

Embedded, automotive, space use it regularly.

I've setup cbmc and goto-analyzer for string searching algos here https://github.com/rurban/smart and really found some bugs in old published algos.