This tool converts Place/Transition Petri Nets from the PNML standard format into the Coq theorem prover language.
Download it from the dedicated page.
PNML to Coq Converter can simply be run on the command line. It is expecting a set of paths to PNML files.
Usage information is available on the dedicated page.