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.

How would you prove stuff about your code like memory safety.

Out of bounds access would raise a runtime exception, so absence of runtime exceptions proves that cannot happen. Recent versions of SPARK add functionality similar to Rust’s borrow checker as well.

You can find more information in the users guide. https://docs.adacore.com/spark2014-docs/html/ug/index.html