> Ada needs a profile that guarantees that code can't be the source of erroneous execution and constrains bounded errors further.

I forgot to add a couple of things in my other comment.

You're conflating a few distinct concepts here.

Ada already provides memory safety by default: bounds checks, range checks, and null checks are all on unless explicitly suppressed. Dereferencing a null access value or indexing out of range raises `Constraint_Error`; it never leads to undefined behavior. So Ada does not need a special profile for that kind of safety.

What you seem to be describing - "a profile that guarantees that code can't be the source of erroneous execution" - is closer to what the SPARK subset provides. SPARK can prove the absence of run-time errors (AoRTE) statically using GNATprove, including ownership and lifetime correctness for access types. That is a verification discipline, not a tasking profile.

Ravenscar, on the other hand, is a concurrency profile. It constrains tasking and protected object behavior to make real-time scheduling analyzable and deterministic; it has nothing to do with preventing run-time errors or erroneous execution. It just limits what forms of tasking you can use.

So: Ada itself is already memory-safe by construction, Ravenscar ensures analyzable concurrency, and SPARK provides formal proofs of safety properties. Those are three orthogonal mechanisms, and it sounds like you're blending them together in your comment. Ada performs its safety checks at run-time by default, whereas SPARK allows proving them at compile-time[1].

I encourage you to read the website for which the link can be found below. If you are serious, then you could go through https://learn.adacore.com as well.

[1] https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce...