He only proves type safety, and layed out ways to prove special type safeties even in type-unsafe code.

He didn't tackle the two other rust unsafeties, memory and concurrency.