Conceptually, a database backing store is just a shared memory. However, modern stores are internally complex, due to the demands of performance, scalability, or fault tolerance; and complexity invites bugs.

Using formal specifications can ensure correctness, but risks being not representative of real systems. Here, we take a formal approach that remains pragmatic: it is grounded in actual database practice and results in a compact, efficient implementation.

We formalise our intuition of transactions, of rich data types, and of store safety. Our analysis exposes the timestamp inversion bug, which was missed by previous formalisms, and a sufficient condition to avoid it.

We go on to specify two basic storage types, map- and journal-based, and prove them safe. This enables us to deconstruct the modern store into a composition of simpler basic stores. Reading the formal semantics as pseudocode, we translate it to Java code, and implement a reasonably efficient clone of RocksDB in only 3 kLoC. We claim an improved understanding of a complex backing store, deconstructing it into simple components, and better confidence in its correctness.