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.