verus

ill be executed, etc."

rocedural macros generate code that can't be statically verified The code that procedural macros generate is visible to these tools and they can verify it well. > interior mutability (`Cell`, `RefCell`) bypasses type system guarantees Although it's indeed harder, some of the tools do support interior mutability (with extra annotations I believe). > Rust can panic in safe code That is not a problem - in fact most of them prove precisely that: that code does not panic. > Most critically, Rust lacks a formal language specification with mathematical semantics That is a bit of a problem, but not much since you can follow what rustc does (and in fact it's easier for these tools, since they integrate with rustc). > Rust's semantics are informally specified and constantly evolving (async, const generics, GATs) Many of those advancements are completely erased at the levels these tools are operating. The rest does need to be handled, and the interface to rustc is unstable. But you can always pin your Rust version. > This isn't tooling immaturity though, it's a consequence of language design. No it's not, Rust is very well amenable to formal verification, despite, as you said, not being designed for it (due to the shared xor mutable rule, as I said), Perhaps even more amenable than Ada. Also this whole comment seems unfair to Rust since, if I understand correctly, SPARK also does not support major parts of Ada (maybe there aren't unsupported features, but you not all features are fully supported). As I said I know nothing about Ada or SPARK, but if we compare the percentage of the language the tools are supporting, I won't be surprised if that of the Rust tools is bigger (despite Rust being a bigger language). These tools just support Rust really well.