Maybe F* with dependent types and proof automation? I am programming in SPARK2014 currently and I would argue it is more of a Rust competitor with a longer legacy in high-integrity, safety-critical programming applications.