There are also efforts at ETH to verify Rust using SMT solvers using methods similar to VCC and Dafny, see https://www.pm.inf.ethz.ch/research/prusti.html

Adding verification once you have code is generally more difficult, though in case of VCC it was helpful to have a large example code base to make sure the tool would cover the major patterns, especially relating to concurrency primitives.