My understanding is that the key feature of SPARK is design-by-contract aka run-time enforced pre- and post-conditions plus invariants for loops. Whereas F* lets you define dependendent types, a subset of which are compile-time constraints similar to those SPARK contracts. Is that a fair contrast?
SPARK's pre-/postconditions and assertions can be statically checked, they aren't just for runtime enforcement. This is its key value proposition, if it were just runtime enforcement it'd be nice, but not that great.
