If you use TLA+ you'll see why this is likely unnecessary. A huge specification, made at three levels of detail, can run to 2500 LOC. Because you have so much control over the level of detail, and because the language is so expressive, there is little need for reuse (except maybe for some common definitions, e.g. of different consistency levels, which are very short but can be non-trivial).
How do you mean unnecessary?
Surely writing such a specification takes many man hours, even after having spent many man hours to learn TLA+? Can none of this effort be encapsulated into something reusable?
The desire for reuse is not driven by a want to reduce LOC, but hours spent.
Most of the effort writing TLA+ is about the what not the how. In general, we know how to make code reuse effective when a lot of implementation hides behind a thin API, but in TLA+ there is no implementation in a meaningful sense. A library of requirements would make about as much sense, and while maybe it's something that could be done, I'm not sure we know how to do it (but if you've seen something like it, I'd love to see it). So maybe it's an interesting idea, but I'm not sure how it would be done. Aside from a utility module that I like including in most of my specs, I never "reuse" modules as is. I often do, however, copy-paste-modify pieces of other specifications, which, I assume, is not unlike how lawyers reuse portions of contracts.
I guess there are occasionally pieces that could be used as-is (e.g. a description of a lossy network), but those tend to be so simple, that looking for them in some Maven-central for spec modules would probably more effort than writing them from scratch every time.
