Non-volatile memory (NVM) is a high-performance memory technology that supports persistency (i.e., durability) of data in case of a system crash (e.g., power failure). For implementations of concurrent objects (e.g., concurrent data structures such as stacks and hash maps), NVM poses a correctness problem: can the implementation recover to a consistent state after a crash and continue execution? In this paper, we study a notion of correctness known as buffered durable linearizability for implementations of periodically persistent concurrent objects, and develop a refinement-based proof method for buffered durable linearizability. To support our proofs, we develop a generic abstract specification of a buffered durable linearizable object that is generated from the object’s sequential specification. Our main case study is a concurrent hash map known as Dalí, which we show satisfies buffered durable linearizability. Specifically, we use FDR, a model checker based on CSP, that offers a fully automatic method for checking trace refinement.