1 Introduction
 1.1 Specification and Programming
 1.2 Interaction with theorem provers
2 Event Logic
 2.1 Events, event orderings, and event classes
 2.2 Inductive logical forms
3 Simple examples
 3.1 Ping-pong
 3.2 Ping-pong with memory
 3.3 Leader election in a ring
4 State machines
 4.1 Moore machines, “pre” and “post”
 4.2 Moore machines with multiple transition functions
5 The two-thirds consensus protocol
 5.1 The specification of 2/3-consensus
  5.1.1 Preliminaries
  5.1.2 The top level: Replica
  5.1.3 ReplicaState and NewVoters
  5.1.4 The next level: Voter
  5.1.5 Round and Quorum
  5.1.6 NewRounds and Voters
 5.2 Illustrative runs of the protocol
 5.3 Properties of the 2/3-consensus protocol
6 Paxos
7 Definitions of combinators
8 Configuration files
9 EventML’s syntax