4 ms·

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 sp

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 https://github.com/mit-pdos/fscq-impl

oggy 11y ago
That's pretty awesome that you could get this verified down to the implementation. We had a related project [1], where we verified a persistent storage system under restarts. Our case study was much simpler than a full fledged file system, and we didn't verify an implementation, but we did also consider hardware failures (partial writes, bitrot, etc). Our proof rules are different though, and I think pretty interesting. But some other choices that we made were in hindsight suboptimal, and some points in your paper resonated with me in a "yup, would do it this way now" way. Really nice work! [1]: http://mynosefroze.com/pubs/fm2014.pdf http://mynosefroze.com/pubs/fm2014.pdf