If there's anyone who works very hard to make formal methods approachable to practitioners, that would be Leslie Lamport. He often says that he's not interested in methods that are not usable by "ordinary" engineers working on large, real-world systems. Amazon now uses his TLA+ to specify and verify many (most?) of their AWS services, and they've learned it all on their own. It's been so successful that managers encourage programmers to use TLA+. This is now spreading to Oracle, too. You can read about Amazon's experience here: http://glat.info/pdf/formal-methods-amazon-2014-11.pdf
I discovered TLA+ when I needed to design a complex distributed database. I learned it in a couple of weeks, and immediately put it to good use. It quickly uncovered some (big!) mistakes in my original idea, and helped me find a solution. So my motivation to learn and use TLA+ was, like Amazon's, 100% pragmatic and not at all academic.
BTW, TLA+ has spread to Oracle because the guy that introduced TLA+ at Amazon (Chris Newcombe) now works at Oracle Cloud (along with a bunch of other senior AWS talent).
I discovered TLA+ when I needed to design a complex distributed database. I learned it in a couple of weeks, and immediately put it to good use. It quickly uncovered some (big!) mistakes in my original idea, and helped me find a solution. So my motivation to learn and use TLA+ was, like Amazon's, 100% pragmatic and not at all academic.