The "big production" example that kept being referred to in university was a (Belgian?) metro system. I think it was well suited to formal verification because it had a finite number of valid states, and the cost of failure was sufficient to justify the investment.

EDIT: I now think it was French, source https://www.prover.com/portfolio-items/ratp-paris/

It's used to some extent in the aviation industry for flight-critical software. So maybe huge in some contexts.