Remote direct memory access (RDMA) allows a machine to directly read from and write to the memory of remote machine, enabling high-throughput, low-latency data transfer. Ensuring correctness of RDMA programs has only recently become possible with the formalisation of rdmatso semantics (describing the behaviour of RDMA networking over a TSO CPU). However, this semantics currently lacks a formalisation of remote synchronisation, meaning that the implementations of common abstractions such as locks cannot be verified. In this paper, we close this gap by presenting \(\textsc {rdma}^{\textsc {tso}}_{\textsc {rmw}}\) , the first semantics for remote ‘read-modify-write’ (RMW) instructions over TSO. It turns out that remote RMW operations are weak and only ensure atomicity against other remote RMWs. We therefore build a set of composable synchronisation abstractions starting with the \(\textsc {rdma}^{\textsc {wait}}_{\textsc {rmw}}\) library. Underpinned by \(\textsc {rdma}^{\textsc {wait}}_{\textsc {rmw}}\) , we then specify, implement and verify three classes of remote locks that are suitable for different scenarios. Additionally, we develop the notion of a strong RDMA model, \(\textsc {rdma}^{\textsc {sc}}_{\textsc {rmw}}\) , which is akin to sequential consistency in shared memory architectures. Our libraries are built to be compatible with an existing set of high-performance libraries called loco, which ensures compositionality and verifiability.