In SPARK contracts can actually be proven (though not all, and not all without effort). So they are a step above plain asserts, or really several steps. Contracts in SPARK are also checked at runtime, which can be disabled if you have proven them either with an automated prover or via some other mechanism (sufficient testing, manual analysis of the code, etc.). Though what can be proven right now is limited so you don't really get the full scope of Ada, but they are constantly working on extending what it can handle.

If you write tests now, the extra notations SPARK introduce aren't much more code than you're already writing, and really it's just entering into the code what you (hopefully) have in your head or on paper elsewhere.