The second section covers the formal verification of the security and resiliency of smart grid control systems by using a formal model to analyze attack evasions on state estimation, a core control module of the supervisory control system in smart grids.