Structured heaps — topological constraints on programs’ memory use, pointers, and references – have been making their way into mainstream programming languages. Rust is based around Ownership Types, External Uniqueness, and Alias Burying; similar facilities have been proposed for Swift; while venerable C++ has had “move assignments” since 2011. This paper reports on our initial experiments using the au- tonomic verification tool Dafny to describe structured heap models, and then to validate those models.