Maybe my memory is faulty but I believe it was analyzed by Leslie Lamports stuff. Ofcourse your building a model of how it should work and you might have faults in that.