There are some things that attempt to come close. Prusti by ETH Zurich is maybe the closest.

https://github.com/viperproject/prusti-dev

https://www.pm.inf.ethz.ch/research/prusti.html

    extern crate prusti_contracts;
    use prusti_contracts::*;

    #[requires(something)]
    #[ensures(result >= a && result >= b)]
    #[ensures(result == a || result == b)]
    fn max(a: i32, b: i32) -> i32 {
        if a > b {
            a
        } else {
            b
        }
    }

Ada seems like a fantastic language though, and the 202x edition brought some niceties to the language.

I am an Ada/SPARK novice, but on first look Prusti seems to deal with contracts, but I am not sure how much more of the Ada/SPARK system it may covergg. I used to dislike Ada and SPARK due to their verbosity, but after studying some of the embedded work in them, and what they bring to the table, I am no longer put off by that or syntax. I've seen Julia and even Elixir projects in areas that would better suit Ada/SPARK, but I think it is due to their popularity rather than applicability. But things like Elixir's Nerves platform is very interesting in bringing the BEAM to the embedded world, and I love Pluto notebooks for Julia, but for high-integrity software I think I'll try and leverage Ada/SPARK's capabilities and pedigree for now. I will look further into Prusti this weekend.

Rust's type system still lacks the expressivity of Ada. Rust has a lot to teach Ada (and you see this coming out from AdaCore's blog recently with efforts to add lifetime analysis to SPARK), but Rust has a ton to learn from Ada as well.

I agree, but I just turned 57 (been programming since 1978 for fun), and there is so much already done in Ada that powers SPARK that it will be a while for it to be tried and true. Although, with all the work on theorem provers and such, maybe it will be exponential and I'll be around to see it. I really like Zig too, but I am staying with Rust because of its inertia. At heart, I love J/APL, but I use them for wholly different reasons.

Interesting work in that direction https://www.youtube.com/playlist?list=PL-uEDsw-7yRLYMEdlvh4u... Rust verification Workshop 2021