This is an unofficial reimagining of the Archive of Formal Proofs
Stellar Quorum Systemsby Giuliano Losa
Abortable Linearizable Modulesby Rachid Guerraoui, Viktor Kuncak and Giuliano Losa