Are there lots of opportunities to work on static analysis and theorem proving outside academia, especially in Silicon Valley?
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.
Some might, but the relevant ISO standards are ok with testing if you reach sufficient coverage, so generally testing is all that's happening.