Abstract
Ensuring the reliability of modern microgrids requires verification beyond conventional simulations. This paper introduces the novel application of TLA+, a formal specification language to model and verify a cyber‑physical microgrid with six DERs and four priority loads. Our approach formally defines critical safety invariants such as Margin of Safety (MoS) ≥ 0 and automatically uncovers subtle design flaws, including MoS violations undetected by conventional testing. Experimental verification on a 25 kV system shows TLA+ can explore 1.79 million states in under 3 minutes, mathematically proving correctness under normal (MoS = +28) and attack scenarios (MoS = –2). State‑space exploration ranges efficiently from minimal configurations (3,332 states, 8 s) to full‑load conditions (1.79 M states, 171 s) with predictable growth indicated by anomaly percentages (0.19 %-65 %). Although validated on a single topology, the method establishes a provably correct foundation for microgrid design, advancing the shift from test‑and‑fix to correct‑by‑construction methodologies in resilient smart grid engineering.