To me, he means that if you take your formally verified program, the axioms do not hold in an environment without memory safety. He isn't saying your formally

To me, he means that if you take your formally verified program, the axioms do not hold in an environment without memory safety. He isn't saying your formally verified program is good in Rust but not in C, he's saying if you put it in the same memory space as an unsafe program, all bets are off. You can formally verify, for example, the BPF engine in Linux, and some other code in the kernel can void that guarantee.