We have formally specified Bully Protocol, a distributed leader election protocol, in Maude, a specification/programming language based on rewriting logic, and conducted model checking experiments with the Maude system that Bully Protocol enjoys a safety property (Non-multiple leader election) and a liveness property (Eventual leader election). Our first version supposes that once a node becomes failed, it will never become active. It is also necessary to use an anti-fairness assumption for Non-multiple leader election model checking for the first version. We have revised the first version such that it is unnecessary to use any assumptions for Non-multiple leader election model checking and failed nodes may become active, and conducted model checking experiments that the revised version also enjoys the two properties. We mainly demonstrate that Bully Protocol does not need to be fully synchronously modeled/implemented and the protocol can be revised such that the node that has the greatest ID among active ones is not necessarily always a leader, which avoids from changing the current leader as a failed node whose ID is greater than the current leader’s ID becomes active.