This repository contains formalizations of the following two PLDI'25 papers:

• "Verifying Lock-Free Traversals in Relaxed Memory Separation Logic": README
• "Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic": README

This work builds upon our prior PLDI'24 work available on the main branch, but it does not support proof automation with Diaframe due to the use of a newer version of Rocq.