Well, for some definition of formal, both state machines and rigorously defined {interfaces|message sequences|protocols} (ie. those with specification-based, generative implementations of endpoints, validating middleware proxies, etc.).

There are two models of reality that I find to be the most useful ones, especially when writing programs. The first is functions, and the second is sequences of states. - Leslie Lamport

... via http://github.com/globalcitizen/taoup

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.