Superconductor electronics (SCE) run at hundreds of GHz and consume only a fraction of the dynamic power of CMOS, but naturally operate on transient picosecond-scale pulses with logic cells that are inherently stateful. When the fundamental units of computation carry state, it requires a rethink of the entire design, simulation, and verification stack. Luckily the principles of programming language design and implementation offer the opportunity of a new, and mathematically well-founded, foundation from which to build. To this end, we propose PyLSE, an embedded pulse-transfer level language for superconductor electronics. PyLSE enables the precise definition of arbitrary SCE cell semantics using transition systems, provides a framework for easily composing these cells into larger designs, and allows for the identification of timing and logic errors through a mix of dynamic checks and sound static analysis. We formalize PyLSE mathematically and demonstrate its capabilities through the design, simulation, and verification of a selection of SCE designs.