Modern decentralized applications often use multiple replicas/copies of data, each of which can be independently operated, to minimize data access latency, provide fault tolerance and improve scalability. Replicated Data Types (RDTs) have emerged as a systematic approach to the problem of ensuring that replicas remain eventually consistent despite concurrent conflicting updates. RDTs provide an elegant solution to the classical problem faced by a distributed system of maintaining an illusion of a centralized system without requiring complete synchronisation. After more than a decade since they were first introduced, RDTs are now widely used in the industry and also remain an active area of research, particularly for the verification problem. In this tutorial, we will first go through the main paradigms of RDT design, namely operation-based CRDT, state-based CRDT and MRDT. We will then focus on the specification and verification problem, going through the two main approaches for specifying correctness of RDTs: an axiomatic, declarative approach, and replication-aware linearizability. Finally, we will present some of our recent work in verifying the correctness of MRDTs targeting both the above forms of specifications.