Formal Verification of Authenticated, Append-Only Skip Lists in Agda: Extended Version

Victor Cacciari Miraldo, Harold Carr, Mark Moir +2

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 th…