Instead of repairing a learned stability certificate after the fact, the network is trained to be verifiable by construction, by differentiating through the CROWN verification bound and making the size of the certified region part of the training objective. On the lossy 39-bus swing model it certifies a larger region than the prior counterexample-guided method (ρ=2.5 vs 1.8) at the same rate, verified three independent ways with zero soundness contradictions, and scales cleanly from a 2-D to a 4-D slice. The open question is how far it climbs toward the full grid state before the verification cost walls out.

A learned Lyapunov function can satisfy its stability condition on 99.98% of sampled states and still fail a formal verifier, because a proof quantifies over an entire region while sampling only ever visits a measure-zero subset. This work shows that gap concretely, 200,000 random samples find no violation where a directed search finds them 6.1% of the time, and closes it with counterexample-guided verification cross-checked three ways (CROWN, Jacobian bound propagation, and dReal SMT). It extends Cui and Zhang's 2022 work on the exact open problem their paper names.