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 u

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