https://www.adacore.com/books/safe-and-secure-software
SPARK is a subset without pointers that feeds information about the program into solvers that prove absence of common classes of errors like overflows and divide by zero. Inspired by Rust, recent work is adding pointers. Praxis' Correct-by-Construction defaulted on Ada with SPARK saved for most critical stuff, esp safety- or security-enforcing.
Right now, Rust is mainly ahead of Ada on dealing with the pointer safety and better safe concurrency. Ada's Ravenscar aimed for safety but was restrictive. That's my take.
Ada/SPARK wins in almost everything else, it has multiple implementations, proven industrial use since early 80's (first standard was in 1983), IDE tooling, it is a common theme in high security computing conferences, libraries for safety critical domains, and people that know the language.
Naturally it has a price disadvantage for FOSS devs that are allergic to GNAT, given that the remaining Ada compilers are well into the enterprise price range.