This article presents the modeling and verification of supervisory energy-management systems (EMSs) for microgrids using timed automata (TA) and a formal verification approach. The EMS plays an essential role in managing the power flow among different components in the microgrid system for its safe and reliable operation. The modeling of the EMS is based on predefined invariants with allowable and nonallowable operating modes, which are the conditions that do not change over time. The failure of invariants could have severe effects on microgrid system functionality, which highlights the importance of verification during the initial stage of EMS design. Conventional approaches, such as simulation and/or experimental verification, require manual checking and skilled professional knowledge to check EMS design correctness. Also, there may be a corner case that could lead to system failure that goes unidentified by manual analysis.