PROMELA, the modeling language of SPIN, is widely used to specify and model check finite-state concurrent systems but lacks support for deductive verification. This paper presents an executable semantics of PROMELA in the \(\mathbb {K}\) framework that enables code-level deductive verification. To address the nontrivial interactions between guarded nondeterminism and concurrency, we introduce Load-and-Fire, an elegant semantic pattern that yields a modular, uniform treatment of guarded nondeterminism, cross-process interference, and atomicity in \(\mathbb {K}\) . Our semantics enables the full suite of analyses provided by \(\mathbb {K}\) , including deductive verification of PROMELA programs with infinite state spaces, a capability previously unavailable for PROMELA models. We illustrate the approach with a case study in deductive verification of an infinite-state concurrent system.