It's not like TLA+ is really pushing research frontiers, it's just a great language using solid established algorithms that works really well for modeling distr

It's not like TLA+ is really pushing research frontiers, it's just a great language using solid established algorithms that works really well for modeling distributed & concurrent systems. Maybe they're unhappy with the proof system part of the language? That's still a research project in progress.