We describe two approaches to use the model checking tool COSPAN to check the hazard freedom in speed—independent circuits. First, we propose a straight forward approach to implement a speed—independent circuit in S/R. Second, we propose a reduction technique over the first approach by restricting the original system with certain constraints. This reduction is implemented on the top of COSPAN which also applies its own reductions, including symbolic representation (BDD).