I'm not aware of any language that can't be improved by this strategy. Amazon even added SMT solving tooling around Rust, because Rust's built-in safety guarantees aren't enough.

I'd say that the added effort is minimal. The compiler spits out more errors. We think a little more carefully about how we write functions so CBMC doesn't complain. There are no silver bullets.

>Satisfiability Modulo theories (SMT) is an area of automated deduction that studies methods for checking the satisfiability of first-order formulas with respect to some logical theory T of interest. It differs from general automated deduction in that the background theory T need not be finitely or even first-order axiomatizable, and specialized inference methods are used for each theory. By being theory-specific and restricting their language to certain classes of formulas (such as, typically but not exclusively, quantifier-free formulas), these specialized methods can be implemented in solvers that are more efficient in practice than general-purpose theorem provers.

>While SMT techniques have been traditionally used to support deductive software verification, they are now finding applications in other areas of computer science such as, for instance, planning, model checking and automated test generation. Typical theories of interest in these applications include formalizations of arithmetic, arrays, bit vectors, algebraic datatypes, equality with uninterpreted functions, and various combinations of these.

http://smtlib.cs.uiowa.edu/about.shtml