Part II — CppVerify

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

• Chapter 9 — Why CppVerify on Clang
• Chapter 10 — Getting started
• Chapter 11 — Your first verified function
• Chapter 12 — Loops in practice
• Chapter 13 — Spec and proof functions
• Chapter 14 — Pointers, frames, and modifies
• Chapter 15 — Toolchain and flags
• Chapter 16 — When verification fails
• Chapter 17 — Backends, modular calls, and debugging
• Chapter 18 — Undefined behavior