Just few hours ago, while driving, I was driving and thinking of one of the books - Little Book of Semaphores. I need to go through some the algorithms and try to formally verify them in COQ, since I'm learning how to do formal proves.