SPARK is free by default, and readily available. You can use it as-is in ada by adding " with SPARK_Mode => On" to your code; here's some examples: https://learn.adacore.com/courses/intro-to-spark/chapters/01...

You can install gnatprove with alire via "alr install gnatprove"

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.

Ada goes beyond memory safety.