Ignoring that the engineering sphere that generally uses Ada works on multi-decade timelines, making Rust a bit too young and immature...
Ada and Rust don't have 1:1 comparison on their safety guarantees.
Rust makes a lot of guarantees around memory safety that Ada does not, whilst Ada is far more focused on correctness. Whilst related, these are very different.
SPARK is a formal proving system for Ada. Formal correctness is what they focus on, that Ada can safely prove mathematically how a function will behave, and how a body of functions will behave.
If you're using Ada without SPARK, it will try and enforce these same guarantees, but generally with a runtime contract system, rather than compile time.
As of Ada 2012, the redesign means that the compiler can make use of the contract information, and was one of the main reasons for a lot of the changes.
Lively, but proprietary. A lot of SPARK stuff tends to be automotive, factory designs, fabrication and the sort of stuff where people working there are buried under dozens of NDAs preventing them from discussing their work in any way.
But projects tend to have a longer shelf-life. Contracts expected to take a decade to complete aren't unusual, and the product can be expected to be in use for twice that, or longer.
Ada and Rust don't have 1:1 comparison on their safety guarantees.
Rust makes a lot of guarantees around memory safety that Ada does not, whilst Ada is far more focused on correctness. Whilst related, these are very different.