Formal Verification of Authenticated, Append-Only Skip Lists in Agda: Extended VersionFebruary 2021
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.
Authors: Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy Steele