Yggdrasil is a toolkit for writing file systems with push-button verification. Yggdrasil asks programmers for three inputs: a specification of the expected behavior, an implementation, and consistency invariants indicating whether a file system image is in a consistent state. It then performs verification to check if the implementation meets the specification. If there is a bug, Yggdrasil produces a counterexample to help identify and fix the cause. If the verification passes, Yggdrasil produces an executable file system. Yggdrasil achieves this automation through a novel definition of file system correctness called crash refinement; it is amenable to SMT reasoning and enables developers to implement file systems in a modular way for verification.



The source code is hosted on GitHub at https://github.com/locore/yggdrasil/.