> you to modularize and reuse pieces of it in the large.

There is no such thing as formal specifications "in the large." The largest software specification ever written in any language that could be fully verified is no more than a few thousand lines (although proofs can be very long). Having said that, I think TLA+ module system is fine; reminds me of ML.

> The second problem is language support. TLA+'s main way of breaking down problems into modules and then using one module as an interface for another (its notion of refinement) suffers from problems analogous to the ones faced when dealing with inheritance.

I don't think so, but if you're modularizing your specs you may be doing something wrong.

> but is rather more annoying to do the opposite, e.g. show that in your new module a single state is meant to correspond to a two states in another module

Right, but the problem here is fundamental. Verifying temporal quantifiers is co-NP-hard in the number of states.

> This means chains of the form A => B, B => C, C => D and therefore A => D (and all the intermediate stages) are somewhat annoying.

Yes, but still about 10x less annoying than writing proofs. :)

> Without robust support for transitive implication, the option of using composition in the traditional composition vs. inheritance debate becomes much less palatable as an option when it comes to inheritance.

Again, using composition is a hint that you may be doing it wrong.

> But there isn't a collection, that I know of, of proved theorems for TLAPS like many other theorem provers.

There are some basic ones here:
https://github.com/tlaplus/v2-tlapm/tree/master/library

Deductive proofs are currently not a viable verification approach in industry (except in some small niches, and/or to tie together model-checking results), so libraries of that kind are mostly useful for researchers who research formal mathematics or deductive verification; that's not exactly TLA+'s target audience. Other proof assistants are used almost exclusively for research or by researchers so they're optimized for that.

> This is mainly because TLAPS itself isn't a prover, but rather delegates to the "magic" methods of other provers.

That's not why (you can choose specific Isabelle tactics in your BY clause). The reason is that the TLA+ proof language was designed to be declarative. I guess some people prefer a more imperative style.

> Another way of stating this is that TLA+ as a language makes it a bit difficult to leverage isomorphisms and homomorphisms to reduce the amount of work you have to do. This is somewhere where alternative logical systems can have a big leg up.

There are many things in TLA+'s design that make deductive verification harder, and many things in other language's designs that makes deductive verification harder. There is no one best way to do this.

I've written about this (a bit more generally) here: https://old.reddit.com/r/tlaplus/comments/abi3oz/using_tla_t...

I think the difference is that TLA+ was designed not for research but for industry use, and so its preferences take into account what's feasible. There is no point making something that few people would do easier at the expense of making something many would do harder.

> Because TLA+ specs are divorced from your codebase, they require far less buy-in to see dividends. You don't have to rewrite your codebase in another language. You don't even have to change your coding practices.

... And because there is no tool in existence that can verify those systems at the code-level anyway, so it's not like there's any other option. You get ~2000-5000 lines of formal spec. You can use them for code and get a tiny program or for a high-level spec formally "divorced" from your code.