Decomposing logic using Hoare triplets and properly incorporating assertions as hints to a model checker wouldn't significantly add time to the development process. There is a lot of misinformation about the supposed overhead of formal methods or the assumption that they must be total. A lot of this is due to the fact that formal methods are typically used in projects where serious harm or death could result from an error, and thus, the cost of verifying the project must exceed the potential risk for failure. An incremental approach is pragmatic and yields results. It does not require the totality of classical formal methods projects.

I have not noticed a significant increase in time for my own development efforts while incorporating model checking into my own software development process. That's anecdotal, but up until the past 10 years, there haven't been many OSS model checkers to choose from. In turn, the cost for using these tools have made it harder to have peer reviewed cost analysis. If using a commercial tool, it's because you were required to do so via FAA or similar. Hence, the adoption curve hasn't yet been wide enough to have the wide adoption you've alluded to. With both the availability of these tools and the increased tool-assisted nature of red team analysis, it'll come.

Language can't fix these problems alone. Not even Rust is a silver bullet here. But, the incorporation of formal methods is an additional layer in a good defense-in-depth strategy.