Formal verification of cP systems using Coq

P systems are widely used to solve computationally hard problems. In this study, we formally verify cP systems (P systems with complex objects) in the Coq proof assistant, and provide a corresponding open source library. To help transform cP notation into Gallina, we propose two sets of modelling guidelines. Comparing to existing P system formal verification studies, our approach shows many advantages and has great potential. To the best of our knowledge, this is the first study to formally verify membrane computing models using an interactive theorem prover.