You won't be able to entirely validate yourself most memory-related invariants in a language which can allow breaking memory safety, that's why I mentioned the

You won't be able to entirely validate yourself most memory-related invariants in a language which can allow breaking memory safety, that's why I mentioned the hypothetical language which can encode proofs for invariants. What you want is effectively automated proof-search (a hard problem) for an entirely-safe systems language (which doesn't even exist yet, AFAIK. at least not what I described).