[wtetzner]

I believe what zozbot234 is saying is that Rust focuses on a specific subset of formal verification, and on trying to make a language with that enforces that subset in a way that is still somewhat ergonomic.

I'm assuming "scalable" in this case is referring to the fact that fully verifying a piece of software is currently takes a large amount of effort. Rust's approach is more "scalable" in the sense that they decided to focus primarily on memory safety, and punted on other forms of verification in the hope that it would be more ergonomic/require less effort.