The CppVerify Book

A guided introduction to formal verification and to writing verified C++ with CppVerify.

Part I develops the core ideas—specifications, program logic, loops, memory, and automated proof. Part II applies them in C++: contracts, the verifier, and the compiler workflow.

• Part I — Foundations
  • Chapter 1 — Correctness and trust
  • Chapter 2 — The limits of testing
  • Chapter 3 — Logic and specifications
  • Chapter 4 — Hoare logic
  • Chapter 5 — Invariants and loops
  • Chapter 6 — Ghost reasoning and lemmas
  • Chapter 7 — Memory, aliasing, and frame conditions
  • Chapter 8 — SMT solvers and automation
• Part II — CppVerify
  • 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