TLA+ is mentioned a lot here and many people point out how it's practically infeasible to use it in real world systems. Just curious, is there any alternative to write specifications which are more closer to common programming languages and can be used by an average programmer to formally prove correctness?
I found this short paper really interesting to understand the fundamental limitations of distributed systems: Consistency Tradeoffs in Modern Distributed Database System Design http://www.cs.umd.edu/~abadi/papers/abadi-pacelc.pdf . The theorem introduced in the paper (PACELC) provides a better way to understand the design of modern distributed systems than CAP.