With others, I am working on formally specifying, implementing and verifying filesystems.
mini-btree, 2021 - now
A new minimal B-tree implementation.
ImpFS, 2019 - now
A new filesystem based on B-trees and persistent logs.
Tjr-kv, 2018 - now
A key-value store for OCaml.
Tjr-btree, 2016 - now
A B-tree-like on-disk datastructure.
mini-fs, 2015 - now
Frontend filesystem components, including FUSE bindings, networking etc.
SibylFS, 2012 - 2015
A formal model of POSIX-like and real-world filesystems, usable as a test oracle.
Some additional resources: