Partial-order reduction (POR) is a technique for tackling the state-space explosion problem in model checking. The search space can be significantly reduced by disabling certain events at the state level. Recent research has brought to light issues in the theory behind several POR approaches. In this work, we demonstrate a method for rigorously testing the soundness of POR theories using Alloy, a SAT-based formal specification tool. We apply this method to several POR theories and formalisms. To explain the modelling challenges that we faced, we show two Alloy models in detail. In our experiments, Alloy manages to produce counterexamples to all theorems that we know to be flawed. This indicates that our ideas are viable for preventing comparable issues in the future development of POR methods.