Static analysis: for sure. Companies with large codebases are interested to understand how their code works, build refactoring tools, find bugs, etc. They have

Static analysis: for sure. Companies with large codebases are interested to understand how their code works, build refactoring tools, find bugs, etc. They have dedicated teams doing this. For example https://github.com/facebook/pfff https://github.com/facebook/pfff. Formal proofs: there are specific applications (see Amazon's use of TLA+). I personally feel nearly every company has a small piece of code that you can justify spending a few weeks/months modeling to ensure its correctness. Also, engineers working on medical devices, avionics, robotics, finance, etc. probably get to prove the correctness of their code.