  This paper describes ongoing work on developing a formal specification of a
database backend. We present the formalisation of the expected behaviour of a
basic transactional system that calls into a simple store API, and instantiate
in two semantic models. The first one is a map-based, classical versioned
key-value store; the second one, journal-based, appends individual transaction
effects to a journal. We formalise a significant part of the specification in
the Coq proof assistant. This work will form the basis for a formalisation of a
full-fledged backend store with features such as caching or write-ahead
logging, as variations on maps and journals.
