To achieve scalability and availability, modern distributed systems often provide only weak guarantees about the consistency of data processing. To help programmers cope with this, researchers have proposed novel programming concepts, such as constructs for strengthening consistency on demand, replicated data types for resolving conflicts (aka CRDTs) and new forms of transactions. These concepts have a subtle semantics and using them correctly remains nontrivial. I will present our ongoing work to develop ways of checking the correctness of their usage. This is joint work with Hongseok Yang (Oxford), Carla Ferreira (U Nova Lisboa), Mahsa Najafzadeh and Marc Shapiro (UPMC).