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).
A very simple set of commands to build many of these components (not
A collection of all ocamldoc documentation is: https://tomjridge.github.io/tjr_imp_build_script/