There is a gap between the formal specification and reality though. We published some work (coincidentally presented right after this paper at SOSP 2015) on bu

There is a gap between the formal specification and reality though. We published some work (coincidentally presented right after this paper at SOSP 2015) on building a real-world mathematical model of POSIX and using it to test existing filesystems; http://sibylfs.io http://sibylfs.io Running SibylFS on Fscq showed up some limitations: - https://github.com/mit-pdos/fscq-impl/issues https://github.com/mit-pdos/fscq-impl/issues (mostly basic missing POSIXisms) - https://github.com/mit-pdos/fscq-impl/issues/2 https://github.com/mit-pdos/fscq-impl/issues/2 an interesting one where the proof about truncate was incorrect in the specification and lead to very weird observable filesystem behaviour. Copy of the SibylFS paper here for the interested; http://anil.recoil.org/papers/2015-sosp-sibylfs.pdf http://anil.recoil.org/papers/2015-sosp-sibylfs.pdf Having said that, these are edges to be polished -- Fscq is an absolutely fantastic advancement in filesystems, and it shouldn't be too many years before we can have a formally verified and specified filesystem in production.