1. 4
    1. 2

      @mjn previously submitted an article on a formally-verified filesystem:

      https://cacm.acm.org/magazines/2017/4/215044-certifying-a-file-system-using-crash-hoare-logic/fulltext

      This work extends that filesystem with I/O concurrency. It also manages to re-use the prior “implementation, specification, and proofs.” That’s often hard to pull off.