It would be really nice given that Schell originally quoted 2 years per system on a verified kernel. The verified ones did always take 1-3 years but just using safe languages on verified kernels could be quicker. Google, Facebook, and Apple have nobody from high-assurance that I'm aware despite their resources. Microsoft Research snagged quite a few but they just build prototypes or tools that most of Microsoft doesn't use. None of the big names care overall that I can tell even though it would help them on certain components. Microsoft at least deployed SLAM intro production for drivers and applied formal verification to parts of Hyper-V. IBM had Paul Karger work with them on a security-enhanced CPU and smartcard OS (Caernarvon) with pieces of both being sold to customers.

Otherwise, I don't know of anything happening with big companies and high-assurance tech. Only smartcard vendors seem to do it regularly for specific components in the hardware (esp MPU's) or software (esp JavaCard or MULTOS).