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.

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.

> Also, engineers working on medical devices, avionics, robotics, finance, etc. probably get to prove the correctness of their code.

Some might, but the relevant ISO standards are ok with testing if you reach sufficient coverage, so generally testing is all that's happening.