It's massively more expensive, so you'll see it used in aerospace, railway signalling, some vehicles (trains, components of some cars), power generation and distribution, industrial processes.

Sometimes also in consumer products that have long warranties and are extremely expensive to recall/repair, like washing machines.

Just yesterday was a post on a formally-verified C compiler, used by Airbus (and others) [2]

[1] https://en.wikipedia.org/wiki/Software_verification

[2] https://news.ycombinator.com/item?id=27648735

This may interest you: https://en.wikipedia.org/wiki/Rice's_theorem

Sure. And if you look at sufficiently small-scale pieces of software, there is probably a lot. As scope of a software system increases, the probability of bugs rapidly approaches unity, though.

Ensuring your requirements are correct is possible, but often hard. Ensuring your software meets the requirements is possible, but often hard, especially if you need to consider hardware failure or defects.

Only in academia