fscq

At least in programming languages, systems, and formal verification project code is both available and often evaluated along side the publication. For example FSCQ(https://github.com/mit-pdos/fscq-impl) from MIT, Verdi (https://github.com/uwplse/verdi) from UW, Dune(http://dune.scs.stanford.edu/) from Stanford, and many more. These are just the areas I work in, its very hard to making sweeping statement about CS as a full field since it is very diverse sub-community to sub-community.

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 Running SibylFS on Fscq showed up some limitations: - https://github.com/mit-pdos/fscq-impl/issues (mostly basic missing POSIXisms) - 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 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

FSCQ is a certified filesystem written and proven correct in Coq. It's the first filesystem with a machine-checkable proof that it's implementation meets its specification and whose specification includes crashes. The full source code of FSCQ is available online: https://github.com/mit-pdos/fscq-impl