Ada is the basis of SPARK, [0] which takes Ada and adds formal verification.
While no doubt massive overkill for 99.9% of applications, there are a small number of use cases (safety-critical or security-critical code) where it can actually make sense.
While in principle you could add formal verification to other languages, I'm not aware of any other such solution with as much mindshare as SPARK. Ada's feature set is already closer to what you need for that purpose than what many other languages offer, so even though SPARK still has to both subset and superset Ada, the same thing with other languages would arguably require both taking more away and adding more.
While no doubt massive overkill for 99.9% of applications, there are a small number of use cases (safety-critical or security-critical code) where it can actually make sense.
While in principle you could add formal verification to other languages, I'm not aware of any other such solution with as much mindshare as SPARK. Ada's feature set is already closer to what you need for that purpose than what many other languages offer, so even though SPARK still has to both subset and superset Ada, the same thing with other languages would arguably require both taking more away and adding more.
[0] https://en.wikipedia.org/wiki/SPARK_(programming_language)