Earlier quoted context omitted.
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).
Sure, but those same speculative execution attacks also trivially defeat ASLR. And practically speaking, memory safety in formally proved software tends to be pretty bullet proof. So, outside of memory unsafety, is there another threat profile where ASLR gains you something?
Sure, consider that the hashCode() of objects in Java are based on memory addresses, which means they’re predictable to an attacker without ASLR.