I've mentioned this a number of times here. AWS uses TLA+ all over the place, and use is strongly encouraged and supported. A service team I worked for had to

I've mentioned this a number of times here. AWS uses TLA+ all over the place, and use is strongly encouraged and supported. A service team I worked for had to implement a back-end process that had zero tolerance for mistakes. The engineers involved had a principle engineer peer reviewed process worked out, and got encouraged to model it in TLA+ as part of that review process given what it was at hand. Two engineers learned TLA+ and PlusCal over the space of about a week, and then outlined the process over the next week or so, and kept finding minor, improbable, correctness bugs. Once fixed, they found translating the code in to actual Java to be very straight-forward "It's fill in the blanks. The whole logical structure is there already". In the end, the feature landed well ahead of planned time, even accounting for the time taken to learn and prove correctness, and was able to be launched with little fanfare and high degrees of confidence. I know at least one of those engineers has gone on to use it very regularly. It gives them a good chance to model the logic first, solving the actual problem at hand, and then start thinking about "the boring stuff" like database connections, unit tests etc.