Yet, it seems nothing has emerged that practitioners actually use. I know that there are some occasional experiments (such industrial team specified their protocols using TLA+/Alloy), but it's still extremely limited. I wonder why that is.
But that's not to say that formal methods are useless! We can still prove some interesting aspects of programs -- for example, that every lock that gets acquired later gets released. I think tools like Infer[0] could become common in the coming years.
[0]: https://fbinfer.com/
I understand that TLA+ is not really intended for that and it's currently used more for super important, mission critical applications like flight computer code, but I would love to see that level of care and attention brought to more typical software, which even in relatively "boring" applications can involve a lot of concurrency nowadays.
BTW TLA+ is not too hard for basic usages. I argue it's much simpler than PlusCal because doesn't have additional semantic layer.
Stated differently, no model can really account for interactions that are invisible to it. As such, unless you are aiming at a giant model that encompasses everything, it seems unlikely that you will be able to use some modeling tools that are made to do this sort of stuff directly.