you said you use Ada, if you use it, you should know that Ada is fundamentally unsafe language with a safe subset called spark.

It could not verify dynamic allocations thats why it has such a huge toolset for working with static allocations.

Frama-C allows you to program in a safe subset of the unsafe language called C.

And these languages are the backbone of everything where lives are at risk. YOu can have a language that allows both unsafe and safe.

Safety is not binary and our trains run C/C++ [BOTH UNSAFE LANGUAGES]