Science of Concurrent Programs
Leslie Lamport
Password Authentication with Insecure Communication
The Part-Time Parliament
Specifying Systems: The TLA+ Language and Tools for Hardware ...