The high proportion of renewable energy sources in power grid will bring huge challenges to the stable operation of the power systems. Compared with the traditional power systems, the energy systems have more complex hybrid dynamic behavior, and the sound formal verification can be used to check the reliability of the system operation. In this paper, energy system models for a single-station operation scenario and an inter-station cooperative operation scenario are established in Simulink. Based on MATLAB Stateflow function module, the weak links of energy station operation are found through formal verification, and the spatial load migration is verified to have a good support for regional energy system reliability. The experimental results verify the effectiveness of the proposed models.