SPIN / Promela Verification
For the "all the processes agree about the one elected leader" part:

It is a combination (conjunction) of 


No more than one process can ever be declared to be the leader: $\Box (\textrm{nr} \_ \textrm{leaders} \le 1).$
Eventually a leader is elected: $\Diamond (\textrm{nr} \_ \textrm{leaders} = 1).$