Well, that's the research question! So far signs are promising, IMO. I think this is at least the best chance formal methods have ever had at being relatively

Well, that's the research question! So far signs are promising, IMO. I think this is at least the best chance formal methods have ever had at being relatively easy to integrate into larger codebases--Rust's type system is strong enough to support nontrivial verification conditions, and effectively encapsulate them, without needing to directly deal with "exotic" logic, heavyweight encodings, pointer obligations that need to be manually discharged, or linking to code generated by some external language (a feature it shares with functional programming languages, as well as "hybrid" linear/dependently typed lanugages, like Dafny or ATS). Unlike functional or dependently typed programming languages, however, Rust has a lot of adoption independently of its suitability for formal methods, meaning that ease of integration has a good chance of benefiting projects that don't have correctness as a principle requirement. For example, assuming that a useful crate can be extracted from this project, it would be quite easy to integrate into a video game like Veloren (e.g. to help improve some of its AI heuristics), which is about as far from traditional high-assurance software as you can get! If we can make using high-assurance software as easy (or almost as easy) as non-high-assurance software, without sacrificing huge amounts of performance to do so, it will be a major step in making software more reliable for everyday programmers, rather than restricting these kinds of techniques to critical libraries like cryptographic primitives where correctness and performance justify pretty much any number of proof engineering hours. This doesn't mean everything would be verified, but with more and more verified "building blocks," less and less engineering time would be spent debugging third party code (which at least IME, is usually much more painful than verifying code at the top level). We have a long way to go to get there, but projects like this are an excellent start.