This project started by revisiting the implementations of communication primitives in Kotlin Coroutines, such as rendezvous and buffered channels, introducing faster and more scalable algorithms, and integrating them into the library. We expanded the project with a CancellableQueueSynchronizer (CQS) framework to implement fair and abortable synchronization primitives. This enables efficient implementations of fundamental synchronization constructs such as mutexes, semaphores, barriers, count-down latches, and blocking pools. Notably, the resulting algorithms come with formal proofs in the Iris framework for Coq.