If an LLM is in fact capable of generating code free of memory safety errors, then it's certainly also capable of writing the Rust types that guarantee this and are checkable. We could go even further and have automated generation of proofs, either in C using tools similar to CompCert, or perhaps something like ATS2. The reason we don't do these at scale is that they're tedious and verbose, and that's presumably something AI can solve.
Similar points were also made in Martin Kleppmann's recent blog post [1].
[1]: https://martin.kleppmann.com/2025/12/08/ai-formal-verificati...