This paper formalises Erlang references as an extension to an existing formal semantics of Core Erlang mechanised in Rocq. We define reference generation based on the evaluation state, rather than relying on a registry of previously generated references. The main advantage of this approach is that it requires considerably less modifications to the existing semantics than the registry-based approach. We argue that references generated this way are sufficiently unique because freshly generated references are guaranteed to be distinct from all references available in the evaluation state at the point of generation. Finally, we present two case studies evaluating our semantics, discuss the advantages and pitfalls of our semantics, and highlight potential enhancements and alternative approaches to formalise references. We also mechanise our results in Rocq.