I actually cannot think of any languages except SML that have complete formal proofs of type safety. Now, I may simply be forgetting something obvious. But Haskell's type systems keeps growing by little features here and there, so no full proof is anywhere; OCaml doesn't have a formal semantics, so it sure as hell doesn't have a proof of type safety (in the usual "a well-typed program doesn't go wrong" sense); Java is unsound (in a particular manner of speaking, of course); C# seems too complicated to have such a proof. The Go authors don't seem the type. Rust is the language in question. Those seem like the big players.
