With others, I am working on formally specifying and verifying filesystems.
So far, we have constructed a filesystem test oracle called SibylFS. The main page for SibylFS is here
We are working on a verified filesystem implementation, including a CoW B-tree library.
A recent poster talking about the different components is:
Many of these components are available from GitHub:
Note that these components in turn require other libraries (which are also available from GitHub).