Part II — CppVerify

These chapters cover verified C++ in practice: the toolchain, contract syntax, common proof patterns, backends (Z3, cvc5, strict portfolio, race, BMC, editable Lean certification), modular calls, how to respond when verification fails, and proving freedom from undefined behavior.

The examples in these chapters write the constructs through the alias cv (cv::pre, cv::check, …) and use the names of <cppverify.h> (valid, seq, set, multiset, map, …) unqualified, as a file does after namespace cv = cppverify; and using namespace cppverify;. The header itself needs no #include. Each complete example is compiled and verified by the test suite, and where a chapter shows verdicts, the example must give them; a few snippets that are part of a larger program are not run.

Verify and compile paths from the same source