Formally verified kernels are pretty rare, and you can always have bugs in verification or side channel attacks that your proofs don’t cover, like speculative execution timing bugs in your CPU. (K)ASLR doesn’t defeat all memory bugs but it helps (a little). It is a very low overhead element of defense in depth that doesn’t require major code changes (unlike say, rewriting your kernel in a memory safe language).