It's been a while since I looked at SPARK and Ada, but the last time I did, SPARK was very well integrated with the GNAT Studio IDE. I still preferred frama-c,

It's been a while since I looked at SPARK and Ada, but the last time I did, SPARK was very well integrated with the GNAT Studio IDE. I still preferred frama-c, because C, but it's a really nice toolchain.