seL4 exhibited great advances in software engineering processes and advances in correctness, zero-copy microkernel IPC performance, and capabilities-based security, but these need explanation, adaptation, and evangelism to real-world use-cases like Linux.

Microkernels have severe limitations when it comes to transactional boundaries of calling multiple subsystems and rolling back on failure.

Linux has too much inertia to reinvent itself instantly or completely into XYZ.

What would add more value would be gradual conversion to Rust and adding formal verification to C and Rust like specifying invariants in comments/metadata like frama-c and/or flux.

PS: Religious judgement opinion wars are rarely constructive.