Among others, Haskell has bottom, unsafeCoerce, unsafePerformIO, and Data.Dynamic. Even in the dependently typed Agda, you have postulates and pragmas like NON_TERMINATING and NO_POSITIVITY_CHECK. Is there any language out there with no unsafe hatches? Even in the most rigorous languages I'm aware of, I don't think 100% guarantees exist.

Some languages get a lot closer than others, though -- I think Elm, Rust, Haskell, and so on are still a big improvement over the status quo of languages. I'd rather get 90% of the way there than 10%.

No. But you the areas of unsafety are explicitly indicated, of limited scope, and not the default.

Also, even in unsafe code, Rust offers more guarantees than many (most?) languages.