How can I formalize key value stores with set theory?
One simple way to model a key-value store is as a map $f:K \to V$ where $K$ is the set of possible keys and $V$ is the set of possible values.

Often, each value $v \in V$ will itself be a tuple or record.  You can represent a tuple as a Cartesian cross-product, e.g., $V = V_1 \times V_2 \times \dots \times V_k$.  You can represent a record as either a tuple (if the set of attributes is finite and known in advance), or as a function from attribute names to values.

Modelling languages like Alloy can represent such maps natively.  Some modeling languages will use the notation $k.f$ instead of $f(k)$ (i.e., object field access notation instead of function evaluation), but the two are equivalent.

If you don't want to use functions, but want to stick to just sets, that is also feasible.  You can model any function $f: K \to V$ as a binary relation, i.e., a set $S \subseteq K \times V$ with the additional property that if $(k_1,v_1) \in S$ and $(k_2,v_2) \in S$ and $k_1=k_2$, then $v_1=v_2$.  However this may be less natural.

This gives you a way to model the state of the store.  You will then need to model the effect of each operation that can be performed on the store, in these mathematical terms.