What I really like about SPARK is the pragmatism. It's not all or nothing, you can call on non-SPARK code, and you don't have to go full functional verification to profit from the SPARK toolset.

edit: if you feel like sharing your code and experience there, I'm pretty sure some people would be interested.