Yes. SPARK/Ada will attempt to verify many of the properties statically. Not everything can be, and not everything can be done without significant effort (that is, more than it may be worth). But it's more than asserts in most other languages which are only verifiable dynamically. For those areas where SPARK can't prove something statically, the checks are used at runtime (like a traditional assert). It's a best of both worlds situation, in that regard.