We investigate the use of the Pointer Assertion Logic Engine (PALE) in the context of Rust. We demonstrate how it is possible to translate Rust’s Mid-Level Intermediate Representation (MIR) into the language PALE, where program annotations and Graph Types are used for semi-automatic formal reasoning over the program store, along with proof of Data Structure Invariants (DI) preservation.We provide a concrete example of modeling an intrusive circular doubly linked list data structure from the Rust-for-Linux project in PALE. We define DI over the said data structure, we attempted to show the absence of memory faults.In conclusion, we find that PALE, along with monadic second-order logic, is an interesting field for further exploration, although our transformation of MIR to PALE lacks a concrete proof of its validity.