CBMC is truly wonderful technology. Rust is still more powerful and easier to use at scale. If your project has 100k lines of code, would you rather use CBMC o

CBMC is truly wonderful technology. Rust is still more powerful and easier to use at scale. If your project has 100k lines of code, would you rather use CBMC or Rust? What about if your project has a million? 10 million? 100 million? The fundamental issue is that SMT-based verification scales quite poorly. The optimal use of SMT-based verification is proving local properties of small chunks of code independently, and using the type system's encapsulation to scale up to global correctness.