Building replicated systems that are both highly available and correct remains a fundamental challenge. Weak consistency models improve scalability and fault tolerance by avoiding coordination at the cost of introducing correctness challenges, such as ensuring convergence and preserving application-level invariants. This research addresses three key problems in this space. First, we plan to develop a coordination-free consistency framework that unifies convergence and invariant preservation under weak consistency models. Second, we will investigate how to safely decompose transactions into smaller executable units to maximise concurrency while maintaining correctness and avoiding observable anomalies. Third, we intend to investigate the automated synthesis of replicated data types that guarantee convergence and the preservation of application-level invariants.