Data Structure Proof in TLA+

Hello all, I was wondering where I can find examples of lock-free data structures being proved to be linearizable in TLA+. I can find examples of programs in the book but not much on data structures. For example, I would love a proof of correctness for the Fomitchev and Ruppert lock-free queue however I can't find anything. I am very new to formal verification. My hope is that I can prove the correctness of my own tree data structure using TLA+. Please let me know of any resources or guides, or if I am barking up the wrong tree / proof software.