Automated planning systems (APS) are maturing to the point that they have been used in experimental mode on both the NASA Earth Orbiter 1 satellite and the Deep Space 1 spacecraft. One challenge is to improve the test coverage of APS to ensure that no unsafe plans can be generated. Unsafe plans can cause wasted resources or damage to hardware. Model checkers can be used to increase test coverage for large complex distributed systems and to prove the absence of certain types of errors. In this work we have built a generalized tool to convert the input models of an APS to Promela, the modeling language of the Spin model checker. We demonstrate on a mission sized APS input model, that we can explore the space of possible plans in Promela and use Spin to verify with high probability the absence of unsafe plans.