Categories: filesystems


With others, I am working on formally specifying and verifying filesystems. I am also working on a verified filesystem implementation called “ImpFS”.

Older work: SibylFS

SibylFS is a formal model of POSIX-like and real-world filesystems, and simultaneously a test oracle which can be used to check real-world traces of filesystem behaviour. The main page for SibylFS is here.

Current work

Title Description
tjr_btree tjr_btree is a Copy-on-Write and Mutate-in-place implementation of a B-tree-like on-disk datastructure.
tjr_kv tjr_kv is a key-value store for OCaml
tjr_minifs Compositional file system components, including FUSE bindings, networking etc.
tjr_impfs The ImpFS high-performance verified filesystem

These components, and many others, are available from github:

Note that these components in turn require other libraries (which are also available from GitHub).

Recent presentations and posters

Related posts: