For each test, for each TLA+ spec, measure percentage of the spec's state space is covered by the test. Accumulate a combined coverage report for each spec.

This might be challenging. There could be billions of states, so tracking whether each one has been covered requires some sort of compression. TLC already does this with "fingerprints" to compress storage of many states, plus something like a Bloom filter? Research how this works.