Bugs in systems software like file systems, databases, and operating systems can have serious consequences, ranging from security vulnerabilities to data loss, and these bugs affect all the applications built on top. Systems verification is a promising approach to improve the reliability of our computing infrastructure, since it can eliminate whole classes of bugs through machine-checked proofs that show a system always meets its specification.

In this talk, I’ll present a line of work culminating in a verified, concurrent file system called DaisyNFS. The file system comes with a proof that shows operations appear to execute correctly and atomically (that is, all-or-nothing), even if the computer crashes and when processing concurrent operations. I’ll describe how a combination of design and verification techniques make it possible to carry out the proof for an efficient implementation.