CppVerify¶

CppVerify is a verifier for C++ that checks your code against the properties you write in the program itself — and reports whether those properties always hold, or shows you when they can fail.

Formal verification lets you treat correctness as an engineering artifact: you state what should be true, and the tool either proves it or gives you a precise reason it does not. CppVerify brings that discipline to everyday C++ without a separate language or annotation dialect.

Contracts in source go through Clang verify and compile paths

Install¶

brew install cmake ninja git
git clone --recurse-submodules https://github.com/SwayamInSync/cpp-verify.git
cd cpp-verify
./setup.sh

→ build/bin/cpp-verify, build/bin/clang++

sudo apt install cmake ninja-build build-essential git
git clone --recurse-submodules https://github.com/SwayamInSync/cpp-verify.git
cd cpp-verify
./setup.sh

→ build/bin/cpp-verify, build/bin/clang++

Install CMake, Ninja, and Git, plus Visual Studio Build Tools (C++ workload).

git clone --recurse-submodules https://github.com/SwayamInSync/cpp-verify.git
cd cpp-verify
.\setup.ps1

→ build\bin\cpp-verify.exe, build\bin\clang++.exe

Manual build (from repository root; same flags as `setup.sh`)¶

cmake -S llvm -B build -G Ninja \
  -DCMAKE_BUILD_TYPE=Release \
  -DLLVM_ENABLE_PROJECTS=clang \
  -DLLVM_TARGETS_TO_BUILD=Native \
  -DCPPVERIFY_VENDOR_Z3=ON \
  -DCPPVERIFY_PREFER_SYSTEM_Z3=OFF
ninja -C build clang cpp-verify

cmake -S llvm -B build -G Ninja `
  -DCMAKE_BUILD_TYPE=Release `
  -DLLVM_ENABLE_PROJECTS=clang `
  -DLLVM_TARGETS_TO_BUILD=Native `
  -DCPPVERIFY_VENDOR_Z3=ON `
  -DCPPVERIFY_PREFER_SYSTEM_Z3=OFF
cmake --build build --target clang cpp-verify -m

cmake -S llvm -B build `
  -G "Visual Studio 17 2022" -A x64 `
  -DLLVM_ENABLE_PROJECTS=clang `
  -DLLVM_TARGETS_TO_BUILD=Native `
  -DCPPVERIFY_VENDOR_Z3=ON `
  -DCPPVERIFY_PREFER_SYSTEM_Z3=OFF
cmake --build build --config Release --target clang cpp-verify -m

Quick start¶

int abs(int x)
  pre(x >= -2147483647)   // every int except INT_MIN, whose negation overflows
  post(result >= 0)
{
  return x < 0 ? -x : x;
}

./build/bin/cpp-verify abs.cpp

./build/bin/clang++ -std=c++17 -fverify-contracts -c abs.cpp -o abs.o

Use -fverify-contracts on clang++ so pre / post are keywords. cpp-verify adds that flag automatically.

Backends and modular calls¶

cpp-verify --backend=bmc --unroll=3 loops.cpp
cpp-verify --dump-ir=3,4 debug.cpp

See Chapter 17 — Backends, modular calls, and debugging for Z3 vs BMC vs Lean export and chained calls like f(g(x)).

Learn more¶

📘 The Book

Foundations (Part I) and using CppVerify on C++ (Part II).

The CppVerify Book

📋 Language reference

Contract syntax and flags.

Language reference

🔧 Verifier API

C++ headers in clang/lib/Verify (Doxygen).

C++ API reference

Source on GitHub