The advent of non-volatile memory (NVM) technologies is expected to transform how
software systems are structured fundamentally, making the task of \emph{correct} programming significantly harder.
This is because ensuring that memory stores persist in the correct order is challenging,
and requires low-level programming to flush the cache at appropriate points.
This has in turn resulted in a noticeable \emph{verification gap}.
%causing a significant verification burden.

To address this, we study the verification of NVM programs, and present \emph{Persistent
Owicki-Gries} (POG), the first program logic for reasoning about such programs.
We prove the soundness of POG over the recent Intel-x86 model, which formalises
the out-of-order persistence of memory stores and the semantics of the Intel
cache line flush instructions. We then use POG to verify several programs that interact with NVM.