It depends how you define "real industrial". Since verification is still very costly, the applications are rather limited to domains as military or air/space transportation.

E.g.. the IMHO most famous and largest project is the seL4 kernel. The was writen in Haskell and proved with Isabell/HOL (and refinded in C). It was used by OK Labs, what was later bought by General Dynamics, world's fifth-largest defence compancy (according WIkipedia).

There are smaller projects in industrial companies. E.g., Daimler Benz once used the OPAL language to develop a proven compiler for ECUs, but I am not aware that the compiler is actual used in non-prototype development (most ECU development is outsourced anyway).

I join Matthias's words, it depends how you define "real industrial".

There were two very large projects, Verisoft and Verisof-XT (http://www.verisoftxt.de), where TU Munich, Univ. of Saarbruecken etc. have verified several parts of real systems and their models, e.g. Microsoft kernel and OSEKtime-like OS.

It was also a formalisation of large parts of the programming language Java and the Java Virtual Machine.

You could read more about verification projects using Isabelle/HOL here: https://isabelle.in.tum.de/community/Projects

I think Green Hill Software's INTEGRITY-178B separation kernel may qualify as a real industrial example. INTERGRITY-178B received EAL6+ High Robustness rating from the NSA. Take a look at the paper " Modeling and Security Analysis of a Commercial Real-Time Operating System Kernel".

The B method has been used for rail safety systems, see

rodin.cs.ncl.ac.uk/Publications/fm_sc_rs_v2.pdf

and

www.methode-b.com/documentation_b/ClearSy-Industrial_Use_of_B.pdf