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.

In this talk, I’ll present some of our work on developing a verified, concurrent file system called DaisyNFS. The system is divided into a transaction system called GoTxn, which handles the key challenges of crash safety and concurrency, and the file-system logic which runs on top. The design enables combining two quite different verification techniques: interactive proofs in Coq and automated proofs in Dafny. For GoTxn’s proof, we develop a new program logic called Perennial for reasoning about crash safety and concurrency, which uses interactive proofs and is built on top of Iris in the Coq proof assistant. For the file-system logic, we implement each file-system operation as a transaction that can be verified using Dafny since it appears to run atomically. The result is a verified implementation of a server that implements the NFS protocol, gets good performance, and has relatively low proof burden for the file-system logic.