Relaxed memory consistency (RMC), the realistic model underlying modern concurrent libraries, departs from the sequentially consistent (SC) behavior that programmers intuitively expect. Verifying libraries under RMC therefore typically relies on two kinds of histories in their invariants to capture the relaxed behaviors precisely: \emph{location histories}, which record the values written to each shared location, and \emph{object histories}, which record data-structure-level events. Invariants that relate these histories obscure the sequentially consistent reasoning that programmers rely on.

To recover intuitive SC-style reasoning under RMC, we present \emph{strict snapshots}, SC-like memory states taken at logical timestamps. The key idea is to interpret history-based RMC memory states as sequences of strict snapshots, enabling SC-style invariants and specifications to be expressed directly on each of these snapshots, leaving only the causal order between memory accesses as RMC-specific reasoning. To make this snapshot usable in separation logic, we introduce \emph{snapshot assertions}, which express separation logic predicates over strict snapshots and support temporal reasoning across time intervals, keeping location histories out of data-structure invariants. Building on these, we formulate SC-style specifications for concurrent libraries that dispense with object histories. Using these techniques, we formally verify Treiber’s stack, the Michael–Scott queue, and, for the first time, a concurrent binary search tree under RMC. All results are mechanized in the iRC11 relaxed memory separation logic built on Iris in Rocq.