where the compiler can guarantee properties of kernel modules instead of requiring hardware guarantees

Then you would need to move compiler to kernel. Well, there is one: BPF(and derivatives). It’s turing-incomplete by design.