@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.
@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.