Designing concurrent objects for non-volatile memory (NVM) is challenging since designers must take both inter-thread synchronization and durability into account. To simplify development, a number of libraries have been developed to support transformations to durability. In this paper, we study one such library, \(\textsf{Mirror} \) , which offers a technique for transforming linearizable (lock-free) concurrent data structures into a durably linearizable version. We aimed to prove soundness of \(\textsf{Mirror} \) using the interactive proof assistant KIV, but in doing so discovered a subtle bug: \(\textsf{Mirror} \) can only be shown to correctly implement a durable compare_exchange_weak instruction rather than a durable compare_exchange_strong, as claimed in the original paper. Unlike the compare_exchange_strong instruction, compare_exchange_weak may fail spuriously. It turns out that the bug in \(\textsf{Mirror} \) ’s implementation is difficult to fix, thus, we only provide a formal proof that \(\textsf{Mirror} \) implements compare_exchange_weak. Our proof is via refinement against an abstract persistency library, \(\textsf{PLib} \) , that we developed in prior work. We split the proof into two steps via a new intermediate specification \(\textsf{IMirror} \) : we prove forward simulation between \(\textsf{Mirror} \) and \(\textsf{IMirror} \) and backward simulation between \(\textsf{IMirror} \) and \(\textsf{PLib} \) . Since any implementation of \(\textsf{PLib} \) is guaranteed to ensure correct transformations to durability, we conclude that \(\textsf{Mirror} \) continues to support this property.