If you are interested in a more nuanced take on what makes unsafe Rust both valuable and difficult, check out my blog post on the Oxide blog: https://oxide.computer/blog/iddqd-unsafe

I directly tackle the concerns you mentioned, and as a followup I'm actually working on formally verifying the library as well (I've had some success and will publish an update regarding this).