This is an unofficial reimagining of the Archive of Formal Proofs
Authenticated Data Structures As Functorsby Andreas Lochbihler and Ognjen Marić
Consensus Refinedby Ognjen Marić and Christoph Sprenger