  The Hashgraph consensus algorithm is an algorithm for asynchronous Byzantine
fault tolerance intended for distributed shared ledgers. Its main
distinguishing characteristic is it achieves consensus without exchanging any
extra messages; each participant's votes can be determined from public
information, so votes need not be transmitted.
  In this paper, we discuss our experience formalizing the Hashgraph algorithm
and its correctness proof using the Coq proof assistant. The paper is
self-contained; it includes a complete discussion of the algorithm and its
correctness argument in English.
