You don’t have to verify your whole application, just set SPARK_Mode => Off where you want to skip it. Alternatively, set the global default to Off and it becomes an opt-in feature.

Proof levels depend on your goals, but most requirements are satisfied by proof of “Absence of Runtime Exceptions” (AoRTE), which is easier than a full formal proof.