End-to-end formally verified solvers for the general relativistic Maxwell and perfectly hyperbolic general relativistic Maxwell equations in curved spacetime, in 1D, 2D, and 3D.