If the tool exists and has minimal overhead, I don't think it is a matter of permission but a matter of necessity. CBMC adds about 30% overhead over just unit testing, in my experience. It does require a different idiomatic programming style to use correctly, and there is a learning curve. Some intuition is required to learn how to use the tool effectively and efficiently, but this can be taught.

For system programming or firmware, it's incredibly useful. I've used this tool in conjunction with threat modeling and attack surface minimization to significantly improve the safety and security of software written in C. At this point, I would not consider working on any C project that did not make use of this tool.

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.