[bluGill]

Is there a free version of SPARK? Proven correct code appeals to me, but I don't enjoy trying to get anything past purchasing.

[ajdude]

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"

[mcguire]

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.

[kevlar700]

Ada goes beyond memory safety.