This project was started with a novel sempahore algorithm for Kotlin Coroutines. After that, we decided to create a flexible abstraction for implementing synchronization and communication primitives. The one is called SegmentQueueSynchronizer and makes the development of such primitives much faster making them simpler and more efficient at the same time. Since we also support abortability of waiting requests (e.g., lock operation can be aborted by timeout) and these algorithm parts are usually the most complicated and error-prone ones, we decided to prove everything formally in the Iris framework for Coq. Now we are completing the proofs and working on experiments, and looking forward to a new paper soon!