This is an artifact associated with a paper called "Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data". The paper associated with this artifact describes the SRDT, a secure replicated data type. To specify exactly how SRDTs work and to verify that they are secure, the paper uses a formal specification implemented in Redex, a library in the Racket language to specify executable formal semantics. The purpose of this artifact is to guide the reader on how to interact with the formal semantics, such that they can explore exactly how SRDTs work, are able to verify the claims of the paper, and are able to reproduce SRDTs for other systems.