[the-smug-one]

TLA+ has been used at Amazon for proving high-level properties of their distributed systems. Very useful, because a fix in prod for a protocol is very costly. ACL2 was used to prove some floating point architecture that AMD used a couple of decades ago haha. Github recently bought the formal methods company Semmle (something like that) for static analysis of repos.

Formal verification is used in critical software, airplanes and so on.

The most popular form of formal methods are type systems, which I would say a normal SWE should learn about and understand. It's not typically characterised as that, but a type system is a proof inscribed in the program for which we guarantee that some properties hold... Sounds pretty formal methodsy to me :-).

It's a specialised area of study, but isn't that the definition of an area of study performed at a university-level?