I didn't read through the linked PDF, but in relationship to work on SEL4, I found [1], it builds on the work that has been done for SEL4, and improves the tool

I didn't read through the linked PDF, but in relationship to work on SEL4, I found [1], it builds on the work that has been done for SEL4, and improves the tools further. As a first example they they implement verified file systems. They managed to implement two file systems: ext2fs and BillyFS. These file systems can be deployed in Linux. Their aim is reduce the cost of verified systems software. [1]: https://ts.data61.csiro.au/projects/TS/cogent.pml https://ts.data61.csiro.au/projects/TS/cogent.pml