This work is focused on presenting a split precondition approach for the modeling and proving the correctness of distributed algorithms. Formal specification and precise analysis of Petersons distributed mutual exclusion algorithm for two process has been considered. The proof of properties like, mutual exclusion, liveness, and lockout-freedom have also been presented.