I find (variants of) QuickCheck https://hypothesis.works/articles/quickcheck-in-every-langua... are pretty good at finding at least a lot of the invariant problems that TLA+ finds, and if you're lucky your language has it integrated already. The F# implementation FsCheck is pretty amazing.