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.

Verified scalar lifetimes¶

CppVerify also tracks initialized local scalar new/delete lifetimes:

int roundtrip(int value) post(result == value) {
  int *p = new int;
  *p = value;
  int observed = *p;
  delete p;
  return observed;
}

Use-after-delete, double-delete, overlapping live allocations, and reads before initialization are proof failures. See Dynamic storage for the bounded local and inferred fresh-owned factory subset.

Address-preserving scalar references¶

Contracted executable free functions may use scalar T& and const T& parameters:

void increment(int& value)
  pre(value < 2147483647)
  modifies(value)
  post(value == old(value) + 1)
{
  ++value;
}

Reference values lower to heap loads, writes lower to stores, and old reads the entry heap. The bounded scalar slice supports direct forwarding, direct *p bindings, ordinary initialized scalar local actuals, and chained local reference aliases. Subobjects, temporaries, reference returns, and non-scalar referents remain fail-closed. See Pointers.

Backends and modular calls¶

cpp-verify --backend=portfolio --cvc5-path=/usr/bin/cvc5 critical.cpp
cpp-verify --backend=bmc --unroll=3 loops.cpp
cpp-verify --lean-fallback=proof hard_goal.cpp
cpp-verify --dump-ir=3,4 debug.cpp
cpp-verify --lower-only --obligation-out=goals.cpv debug.cpp
cpp-verify --obligation-in=goals.cpv --backend=z3