I think formal verification can and should be used everywhere it is helpful, which certainly includes hard realtime systems but isn't limited to them (it's helpful in quite a few areas). But formal verification is by no means the same as deductive theorem proving. Especially for hard realtime systems, which tend to be simple as you say, model-checking has been the formal method of choice for decades.
Even for large, non-critical software, there are useful formal verification methods that aren't end-to-end, i.e. they can cover the design but not the code, and have proven very useful in finding bugs. I for one, am a big fan of TLA+. TLA+ has both an interactive theorem prover and a model checker (or a couple). Most importantly, it allows describing the system at an arbitrary level of detail, which means you can use it at different levels as appropriate. For some things, it can and should, say, describe hardware in full detail; for others, it can be used to describe and verify a very abstract algorithm, well above the code level.
The problem with deductive theorem proving is that it tends to have a low ROI, and there are often more effective methods. It should be used when other methods don't work well.
Even for large, non-critical software, there are useful formal verification methods that aren't end-to-end, i.e. they can cover the design but not the code, and have proven very useful in finding bugs. I for one, am a big fan of TLA+. TLA+ has both an interactive theorem prover and a model checker (or a couple). Most importantly, it allows describing the system at an arbitrary level of detail, which means you can use it at different levels as appropriate. For some things, it can and should, say, describe hardware in full detail; for others, it can be used to describe and verify a very abstract algorithm, well above the code level.
The problem with deductive theorem proving is that it tends to have a low ROI, and there are often more effective methods. It should be used when other methods don't work well.