That's true in its current state. Remember, though, that they're working on multithreading in a way that ties into their proof from high-level spec down to the

That's true in its current state. Remember, though, that they're working on multithreading in a way that ties into their proof from high-level spec down to the code down to the assembly. Googles people are just putting together a kernel with review & testing. They could take seL4, modify it for concurrency, check it with concurrency-related tooling, and still get quite a bit of assurance from original work. Proof no longer applies but most things it applied to haven't changed. And model-checkers for concurrency are among easiest tools to use in formal verification w/ TLA+ getting adoption even by mainstream companies.