"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