Interestingly both Frama-C and SPARK use linked list as an example. But yes, not everything can be verified, though I'd rather bet on Ada than Rust in this area.
https://blog.adacore.com/pointer-based-data-structures-in-sp...
Yes, I could and should have been more explicit when I spoke of 'linked lists' without further qualification. While talking about these languages designed to eliminate all ambiguity I would do well to be unambiguous. :-)