First, using plain TLA+ does make modularity easier.
Second, I think you should consider whether composing modules is really what you need. After all, specifications should be short. Modules are great for various utility and general definitions that you may want to share among different refinement levels of your spec; they're also great to demonstrate the theoretical power of TLA+; but for practical, non-research purposes (whether you use the model checker or the proof system), I've found that if you want to specify multiple functional components, composing modules may be overkill. It's better to do the following: Specify each component as a separate specification, check it, but then, in the top-level spec, instead of actually using the component modules, use a short definition that specifies the external behavior of those components at a higher level of abstraction.
Ron