A great introductory tutorial on distributed systems formal verification using TLA+. Even though FV and model checking is overkill for many of web services, it is a tool that an engineer should keep in his/her toolbox : one day it might become handy!
Great analogy between consistency models and memory models
A study from 2016 of consistency models for non-transactional distributed storage.