How can I formalize key value stores with set theory? I'm currently developing a simple key-value NoSQL store and want to build its formal model. I'm interested in knowing if there some work about formalization of key-value stores outside of category theory? I want to use some more simple and lightweight mathematics for the mathematical description of key-value stores. Set theory looks like it might offer some possibilities.
You did not say why you want a formalization, but presumably you want to do things with it, for instance prove properties of dictionaries and operations on them. In fact, your question can be understood in two ways: you want a mathematical description of dictionaries, or you want a computer formalization of dictionaries.

For a computer formalization have a look at the Coq standard library module FMaps, and if someone can find something better, please post it in the comments or just edit this question.

For a mathematical description all you have to note is that a dictionary is the same thing as a mapping with a finite domain. That is, if we have a dictionary (using Python style syntax):

d = { 'a' : 1, 'b' : 3, 'c' : 2 }


that is the same thing as a map $d$ whose domain of definition is the set $\{a, b, c\}$ and is defined as:
$$ d(a) = 1, \quad d(b) = 3, \quad d(c) = 2.$$
So now you can take any mathematical description of a map and use that. In set theory we would say that $d$ is the set of ordered pairs
$$\{(a,1), (b,3), (c,2)\}.$$