As some other people have pointed out, you have to pick the domain and application. Airbus controllers (abstract interpretation [1]), Microsoft software driver verification (SLAM model checker [2]) were ones where formal methods found use in the pre-2010 era. Since then, the domain has led to work that brings Excel the capability to auto fill data [3], toy demonstrations of how synthesize programs while verifying them correct [4], verify file systems [5], and now verify and synthesize smart contract code (whose deployments are expected to be permanent) [6]. This is just a sampling. There are many of other uses.

[1] Astree http://www.astree.ens.fr

[2] SLAM SDV https://www.microsoft.com/en-us/research/project/slam/

[3] flashfill https://www.microsoft.com/en-us/research/blog/flash-fill-giv...

[4] Invariant based synthesis https://www.microsoft.com/en-us/research/wp-content/uploads/...

[5] FS verification https://www.usenix.org/conference/atc17/technical-sessions/p...

[6] Solidity verification and synthesis https://synthetic-minds.com