Formal verification of elliptic curves. Depence on the equation form
For instance, say I do the verification for Weiertrass form and then I "convert" the results to Edwards form. Would this be still side-channel attacks resistant?


Well, if you have a Weierstrass form and an Edwards form of the same curve, they're actually the same group, with an easily computable isomorphism between the two, and so any group property (including things such as the difficulty of the discrete log problem) would be preserved.

However, you specifically asked about side channel resistance; that's not a group property.  Instead, it is a property of the implementation (as a side channel attack listens into internals of the implementation as it computes).  If you have two different implementations of the same curve (for example, a Weierstrass implementation and an Edwards form implementation), then proving that one of your implementations is resistant to a specific side channel attack says nothing about whether your other implementation is.