PyLSE is a Python-embedded pulse-transfer level language for the design and simulation of superconductor electronics (SCE). SCE are an attractive alternative to CMOS because of SCE's low power dissipation and ultra-high switching speed, but unfortunately they are difficult to design for due to their pulse-based information encoding and stateful nature. The purpose of PyLSE is to make it easier to create precise and composable models of the basic SCE cells (i.e. gates), use these models to create larger systems, quickly get up and running in the built-in simulation framework, and finally prove various properties about these cells and systems using a state-of-the-art model checker. This artifact will show you how to do so, as well as show you how to get the results in the tables and figures found in the evaluation section of our paper.