I haven't seen those papers. The general thought seems to be that progress is good enough that a restricted subset of C++ can be proved (which is getting less restricted all the time, though probably never will be everything) and the solvers will be able to detect where they give up: if you want a solver you will have to write the code they can prove and that is an acceptable limitation.

Contracts also allow a solver to say "I can't prove this messy function, but I can at least prove everything around it". Which is to say if we prove the precondition is met, and if we assume the post conditions are met, we can prove everything else despite the messy parts we can't do. This at least lets us know where the messy code is.

"Verified Design-By-Contract" has been implemented for C/C++ (annotated subset) by David Crocker in his Escher C/C++ Verifier - https://www.eschertech.com/products/ecv.php and https://www.eschertech.com/products/verified_dbc.php

More links in my previous comment chain here - https://news.ycombinator.com/item?id=48544022

The basic idea is that you generate "Verification Conditions"(VCs) by mapping the function onto a Hoare Triple viz. {Pre} Function-Body {Post} and then applying Dijkstra's WP-Calculus mechanically to step backward from the Post to the Pre thus generating a mathematical formula.

The programmer provided contracts are merged into this formula to generate the complete VC which is a logical implication viz; Pre ==> WP(contracts-from-function-body, Post).

This is then handed off to a automated solver which verifies that Post is met when Pre is True in all the paths.

See also, Combining Tests and Proofs with Contracts for Better Software Verification - https://news.ycombinator.com/item?id=50108206