FSCQ is the first file system with a machine-checkable proof
(using the Coq proof assistant) that its implementation meets its
specification and whose specification includes crashes. FSCQ provably avoids
bugs that have plagued previous file systems, such as performing disk writes
without sufficient barriers or forgetting to zero out directory blocks. If a
crash happens at an inopportune time, these bugs can lead to data loss.
FSCQ's theorems prove that, under any sequence of crashes followed by
reboots, FSCQ will recover the file system correctly without losing data.
Using Crash Hoare Logic for Certifying the FSCQ File System
Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich.
Specifying crash safety for storage systems
Haogang Chen, Daniel Ziegler, Adam Chlipala, M. Frans Kaashoek, Eddie Kohler, and Nickolai Zeldovich.