Formal verification of authenticated, append-only skip lists in Agda
Victor Cacciari Miraldo, Harold Carr, Mark J. Moir, Lisandra Silva, Guy Lewis Steele · 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.