The Ada language allows for a subset of the language called SPARK (not to be confused with the Java framework). In Ada you can do Design-by-contract but in the

The Ada language allows for a subset of the language called SPARK (not to be confused with the Java framework). In Ada you can do Design-by-contract but in the SPARK subset you can actually formally prove the implementation's correctness. SPARK is used to my knowledge in rail signalling system, air traffic control systems, Class III medical devices, and now also NVDIA plans to use it for sections of their ADAS platform. I think the cost aspect is overblown. The biggest issue is that anything related to Ada is not really that well known and often what is known is based on stereotypes from the 80's. Also for most people they would not see it as career growth move to switch to an Ada based technology stack.