The paper Adaptive Linear-Space Renaming by Delporte-Gallet, Fauconnier, Gafni, and Lamport appeared in Proceedings of the 27th International Symposium on Distributed Computing (DISC 2013). Its algorithms were written in PlusCal and specified in PlusCal and TLA+. Formal TLA+ proofs of their safety properties were written. They were completely checked by TLAPS, the TLA+ Proof System. except that:
The proofs are best read hierarchically using the TLA Toolbox.
Stephan Merz aided in writing the TLAPS proofs.