http://lara.epfl.ch/~kuncak/
This is an unofficial reimagining of the Archive of Formal Proofs
Abortable Linearizable Modulesby Rachid Guerraoui, Viktor Kuncak and Giuliano Losa
File Refinementby Karen Zee and Viktor Kuncak
Binary Search Treesby Viktor Kuncak