PyNuSMV is a Python framework for experimenting and prototyping BDD-based model checking algorithms based on NuSMV. It gives access to main NuSMV functionalities, like model and BDD manipulation, while hiding NuSMV implementation details by providing wrappers to NuSMV functions and data structures. In particular, NuSMV models can be read, parsed and compiled, giving full access to SMV’s rich modeling language and vast collection of existing models.