I think it might be possible to write a TLA+ parser and generate QuickCheck tests from it that will exercise invariants at least.