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/