I know about seL4. It is a microkernel. That means it doesn't do most of the things a normal kernel does. It does not contain a file system, nor a networking stack, nor authentication and rights management, nor hardware abstraction and IO. It only does virtual memory management (providing an address mapping for processes), process scheduling, and a very simple form of IPC. Matter-of-fact, the primary author of L4 worked at the same research lab as I did, and before that worked with my best friend from high school when working at the GMD.
I don't want to minimize the accomplishment of those people; being able to prove 10K lines of code to be formally correct is absolutely heroic, and a milestone in that field of research. But 10K lines of code are not an OS. Correctness proofs for something as big as a useful general purpose OS (at least for a server or router, even without UI) is still far from possible today.
Similarly, the algorithms from Dijkstra's old book are nice. In particular it's nice to watch how he reasons about each algorithm, and verifies it as he goes. Today we do much of the same thing ... the idea of adding checks pre- and post-conditions (a.k.a. "assert") is to some extent an outcome of that book. But Dijkstra's vision is nowhere near for practical-size programs, except in very specialized environments (trusted computing infrastructure in infosec, and extreme reliability code for things like the space shuttle life support control system). Very little code is formally verified today (sadly).
And you know, from the standpoint of OpenBSD, FFS as a file system really is good enough. OpenBSD is not intended to be the next Linux or Windows, it does not want to reach 90% market share, nor does it want to run on high-performance computers. It is intended to be a small but functional Unix implementation, with full networking and server infrastructure, and a basis for a functioning GUI. It does that really well, as long as you don't have requirements that are outside the things it wants to do. If you absolutely need ZFS or something (because you want to build a file server appliance that is protected against undetected disk read errors and has CRC on the data path), don't use OpenBSD. If you want full scalability to processors with many cores, don't use OpenBSD. If you have unusual hardware (like I had a newish wireless card I was trying to use an AP), don't use OpenBSD. But for the things OpenBSD is intended for, FFS does the job, and it's old, well-tested, and reliable.
