Categories: filesystems


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 path_resolution or mini-fs) is:

A collection of all ocamldoc documentation is:

Related posts: