A formal safety controller synthesis method for power grid frequency regulation using energy storage systems is proposed. After a fault, with uncertainties in the fault clearing time, the generator machine angles and rotor speed deviations will enter a set of post-fault states that can be over-approximated using reachability analysis. We use the robust neighbourhood approach to cover this set using the initial robust neighbourhood of finitely many simulated post-fault trajectories. We design these simulated trajectories to meet the frequency regulation requirements specified in Metric Temporal Logic (MTL) by optimizing the input signals through a functional gradient descent approach. In this way, all the possible post-fault trajectories with the given uncertainties in the fault clearing time are guaranteed to satisfy the MTL specification. Further, a piecewise linear control law is learned from the data of the simulated trajectories to generate a feedback controller that is more reactive to unexpected disturbances.