Memory safety is only a subset of verification. In fact, most programming languages are memory safe (although I think there are no formal proofs, I haven't come

Memory safety is only a subset of verification. In fact, most programming languages are memory safe (although I think there are no formal proofs, I haven't come across memory unsafety in a language that claims to be memory safe). seL4 is actually another verified software I know.