Comment by kobebrookskC3

you wanna verify all your c just for memory safety? i bet you if you actually tried to verify c for memory safety, you would come screaming back to rust.

and also seL4 is about 10k lines of code, designed around verification, sequential, and already a landmark achievement of verification. linux is like 3 orders of magnitude more code, not designed around verification, and concurrent.