  Authenticated Append-Only Skiplists (AAOSLs) enable maintenance and querying
of an authenticated log (such as a blockchain) without requiring any single
party to store or verify the entire log, or to trust another party regarding
its contents. AAOSLs can help to enable efficient dynamic participation (e.g.,
in consensus) and reduce storage overhead.
  In this paper, we formalize an AAOSL originally described by Maniatis and
Baker, and prove its key correctness properties. Our model and proofs are
machine checked in Agda. Our proofs apply to a generalization of the original
construction and provide confidence that instances of this generalization can
be used in practice. Our formalization effort has also yielded some
simplifications and optimizations.
