If you squint hard enough your example does look a lot like Ada pre and post condition contracts (perhaps a bit less ergonomic, at least for someone who hasn't written C++ in a while).

At this point the rust contracts crate with requires/ensures looks like a more straightforward approximation of Ada's Contracts and assertion policy. But still as far as I am aware no one has implemented something that mimics the static proof functionality in Ada's SPARK subset (which arguably not all applications or problem domains actually need or can justify the extra effort/cost).