Wow. Did not anticipate such a long reply thread. Man it looks like I really should write up a comparison of my (amateur) experiences with TLA+ (TLC + TLAPS), Dafny, Idris, and Liquid Haskell.

Also permeakra, regardless of whether you agree with the points that pron is making here, if you ever find yourself interested in TLA+, I would highly recommend his four part TLA+ series (potentially as an intermediate step after e.g. Lamport's video course). It's absolutely fabulous.