Filesystems

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:

• Conference talks on YouTube

• Blog articles