A solution might be to have a library of boosted specifications. For
example a specification of a sorting algorithm but with a piece of
code behind to speed up TLC.
The only good reason to write a library module to aid model checking
is to define operators that TLC can't handle (except perhaps at
exorbitant computation cost) without overriding the definition with
Java code. For example, it seems to be impossible to define Seq so
that TLC can evaluate the _expression_ seq \in Seq(Nat) when seq is a
sequence. For example, there was no need for the standard Bags
The problem of writing a sorting operator that TLC can evaluate
efficiently is discussed in Section 9.2 of the Hyperbook. The
definition given there is five lines long. The time-complexity of
that algorithm is O(n^2). If you need a more efficient algorithm, you
could find one in an algorithm book somewhere and code it as a
recursively defined TLA+ operator. But if O(n^2) isn't good enough,
you are probably using TLA+ to do things it wasn't meant to do.