&gt; How can I know that my sync algorithm works?<p>TLA+ is one such language that can help you. It models computation at a higher level using the <i>Temporal Logic of Actions</i>. Essentially you define some variables to model your problem in and declare a bunch of next-state relations. You can then check your design against your correctness and liveness invariants to see if your expectations hold against all possible executions.<p>If you are so inclined you can even go as far as proving it correct.<p>I recently just grasped the proof of the strong-fairness property and it&#x27;s amazing to me that we don&#x27;t use predicate and temporal logic more frequently in software development.<p>There are other languages of course such as Event-B and Z, but I find for learning these concepts TLA+ is a great introduction.<p>[0] <a href="https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=iCRqE59VXT0" rel="nofollow">https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=iCRqE59VXT0</a>