VMCAI 2018: “Co-Design and Verification of an Available File System”

Formally verifying the properties of a distributed file system, with Availability under Partition  properties.  The file system consists of interdependent CRDT objects under a strong safety invariant (tree shape).  Paper by Mahsa Najafzadeh, Marc Shapiro and Patrick Eugster, published at VMCAI 2018.  The paper is available here.