Sure, but that's somewhat orthogonal to my point. Yes, you could basically do anything that TLA+ does inside of Isabelle (more familiar with that one than Coq)

Sure, but that's somewhat orthogonal to my point. Yes, you could basically do anything that TLA+ does inside of Isabelle (more familiar with that one than Coq), but it's harder. I think what makes TLA+ interesting is that an engineer with basically no understanding of anything more complex than "I basically know what a set is" can be useful within an afternoon or two. I love Isabelle but it's got a substantially steeper learning curve than TLA+. I'm not saying it's unnecessarily steep, because Isabelle is a lot more versatile than TLA+, but as a result it's a fairly difficult sell for employers, at least in my experience.