As a Frama-C developer, and more precisely the deductive verification tool, I'd say that formal proof of programs (especially proof that the program conforms to its specification) would be significantly easier on Rust. The main reason is related to the handling of memory aliases which is a nightmare in C, and that generates formulas that kill SMT solvers. The consequence is that the ongoing development tend to target something that has a lot in common with Rust: we try to assume memory separation most of the time, and check that it is true on function call, but it as harder to do it than with a type system.
> the handling of memory aliases which is a nightmare in C
Zig has some aliasing issues which are to-date unsolved. The core and community are keenly aware of them, and they'll be solved or greatly ameliorated before a 1.0 release. It's why TigerBeetle has a coding standard which requires all container types to be passed by constant pointer, not reference.
It isn't ideal, but I think it's reasonable to withhold judgement on a pre-1.0 language for some sorts of known issues which are as yet unaddressed. It's worth taking the time to find an excellent solution to the problem, rather than brute-force it or regress one of the several features which combine into the danger zone here.
If you're curious or interested in the details, look up "Attack of the Killer Features" on YouTube. Given your background, I'm sure the community would value your feedback on the various issues tracking this.
