I think Rust has a good chance to take away market share from Ada and Ocaml. Its eco system (packages, documentation) is more comprehensive already thanks to its broader appeal and being in fashion. I don’t see why stronger verification should not appear at some point. Progress and need is there.