veripp

AI-operated formal verification for real C and C++ code.

veripp wraps the ESBMC model checker in an LLM agent loop so that a regular C or C++ developer can run:

veripp verify src/parser.cpp --function parse_header

and get back one of three things:

1. A proof — the property holds (with the bounds and assumptions stated explicitly).
2. A bug — a concrete counterexample trace, minimized and explained in plain language.
3. A question — e.g. "this fails only when len == 0; is len > 0 a precondition?"

The division of labor is strict: the LLM only proposes, the solver disposes. Harnesses, loop invariants, and preconditions suggested by the model are always checked by ESBMC before anything is reported. A hallucination costs a retry, never soundness.

Get started

Pick whichever suits you; all three run the same checker.

# 1. A container, needing nothing else installed
docker run --rm -v "$PWD:/src" ghcr.io/gfabbretti8/veripp scan src/parser.c

# 2. The CLI, if you have uv and ESBMC (see Requirements)
uv run veripp scan src/parser.c

# 3. As a skill your coding agent can use, needing only Node
npx veripp-skill

Then, on this repository's own examples:

uv run veripp doctor                                                # is the checker sound?
uv run veripp verify examples/ring_buffer.cpp --function push       # proves a postcondition
uv run veripp verify examples/off_by_one.cpp  --function sum_array  # finds a real bug
uv run veripp scan   src/                                           # a whole project

Exit codes: 0 verified, 1 counterexample, 2 usage, 3 inconclusive — so CI can act on the result. An inconclusive run is not a pass.

What a result looks like

Result: counterexample
  bounded, unwind=8; checks: overflow, bounds, pointer, div-by-zero; std=c++17
Assumptions (a result is only as good as these):
  - `a` points to exactly `n` valid elements, with n <= 4 (harness bound on array length)
Violated property: dereference failure: array bounds violated
  at examples/off_by_one.cpp:7:9 in sum_array
Counterexample inputs:
  n = 4
  a_buf[0] = -1879048911
  ...

Exit codes: 0 verified, 1 counterexample, 2 usage error, 3 inconclusive.

Requirements

• uv (it installs Python for you)
• ESBMC built from master, or the weekly build (which, despite the name, is cut infrequently — check its date). Not the v8.4 release — it carries esbmc#6508 and silently misses out-of-bounds writes in ordinary container code. veripp doctor checks this for you. On macOS: brew install --HEAD esbmc.
• An LLM, only for triage — see below. --no-llm runs the plain verifier pipeline with no model at all.

ESBMC is a C++ binary, not a Python package, so uv cannot install it. If you would rather not think about that at all, use the image — it carries a checker that has already passed the soundness probe at build time:

docker run --rm -v "$PWD:/src" ghcr.io/gfabbretti8/veripp scan src/parser.c

Otherwise install it yourself:

brew install --HEAD esbmc    # macOS. NOT `brew install esbmc`, which is 8.4.
# Linux x86_64: download esbmc-linux.zip from the `weekly` release above,
# unzip it, and put the binary on PATH.
# Linux arm64: no prebuilt ESBMC is published; use the image.

veripp doctor checks all of the above, tells you what is missing, prints the right command for your machine and architecture, and probes your checker for known soundness holes.

Shell completions are generated from the CLI itself, so they cannot fall out of step with it:

eval "$(veripp completion bash)"      # or zsh
veripp completion fish | source

Why

Model checkers like ESBMC and CBMC are sound and mature, but they need an expert operator: someone to write the verification harness, guess loop invariants, interpret counterexample traces, and decide how to escalate. That labor is why formal verification is still a specialist activity. veripp's bet is that an LLM can be that operator, and the solver keeps it honest.

Architecture

┌─────────────────────────────────────────────────────────┐
│ 4. Interface     CLI · JSON output · GitHub Action ·     │
│                  cache keyed on function-body hash       │
├─────────────────────────────────────────────────────────┤
│ 3. Agent loop    attempt → triage → escalate (budgeted)  │
│                  any LLM proposes preconditions; ESBMC   │
│                  checks every one, and vacuous proofs    │
│                  are rejected                            │
├─────────────────────────────────────────────────────────┤
│ 2. Specification implicit properties (overflow, bounds,  │
│                  UB, null deref — free) + explicit       │
│                  contracts via veripp/contracts.hpp      │
├─────────────────────────────────────────────────────────┤
│ 1. Ingestion     compile_commands.json for include paths │
│                  and defines; harnesses built from the   │
│                  signature; unlinked callees disclosed   │
└─────────────────────────────────────────────────────────┘

Status

Working and used on real libraries. veripp harnesses a function, a whole class (as a call sequence), or every function in a file; reads compile_commands.json; triages counterexamples with any LLM; and refuses to call a vacuous or unsoundly-obtained result a proof.

Measured across nine popular C libraries — 40 of libpng's 70 functions proved, 99 of lodepng's 260, 32 of cJSON's 117 — free of overflow, out-of-bounds, null dereference and division by zero for any input within the stated bounds.

Those counts were taken with the four checks veripp ran at the time. It now checks eight properties by default. Re-running cJSON with the same build and bounds, changing only the check set: 32 proved under four checks, 31 under eight — the stricter set cost exactly one proof, and cost it to internal_malloc, whose body is return malloc(size) and which the memory-leak check flags because the harness never frees. veripp labels that a harness artifact rather than a bug. Details and the per-check false-positive measurements are in benchmarks/CORPUS.md. Full table, and the veripp bugs each library exposed, in benchmarks/CORPUS.md. See ROADMAP.md for what is not done, and Known limits below for what to expect before you point it at your code.

See it find a real CVE

./demo/cve-2019-13223/run.sh        # a few seconds, clones stb for you

veripp rediscovers CVE-2019-13223 — a division-by-zero in stb_vorbis's predict_point(), reachable from a crafted Ogg Vorbis file — on the real, unmodified upstream source, then proves that the precondition the official fix enforces (x1 != x0) eliminates it. In agent mode the triage proposes that precondition itself; the solver confirms it. See demo/cve-2019-13223.

Bring your own model

How well does the triage actually work? The path is validated end to end against a real model, and a 7B local model scores 0/2 on the benchmark. No hosted model has been graded here — see benchmarks/TRIAGE.md for exactly what is and is not evidenced, and the one command that closes it.

Triage works with any provider, and veripp needs no extra packages for most of them — everything except Anthropic speaks the OpenAI-compatible HTTP API, which veripp calls with the standard library.

veripp verify src/parser.cpp --function parse   --model openai:gpt-4o-mini
veripp verify src/parser.cpp --function parse   --model gemini:gemini-2.0-flash
veripp verify src/parser.cpp --function parse   --model groq:llama-3.3-70b-versatile
veripp verify src/parser.cpp --function parse   --model ollama:llama3.1   # local, no account
veripp verify src/parser.cpp --function parse   --model anthropic:claude-opus-5

Built-in: anthropic, openai, gemini, groq, together, deepseek, mistral, openrouter, ollama, lmstudio. Anything else that speaks the same API — a self-hosted gateway, vLLM, Azure — works with --llm-base-url https://…. Defaults come from $VERIPP_LLM_MODEL and $VERIPP_LLM_BASE_URL; veripp doctor lists which providers have credentials.

A small model is a reasonable choice here. Every proposal is re-checked by ESBMC, so a wrong guess costs a retry, not a wrong answer. benchmarks/eval_triage.py --models a,b,c scores providers against known answers so you can pick on evidence.

In CI

- uses: gfabbretti8/veripp@main
  with:
    source: src/parser.c
    fail-on: never      # report findings without failing, for a first run

It installs ESBMC (the weekly build, since the release is unsound for a pattern veripp targets), runs veripp doctor so a broken checker fails the job rather than producing quiet non-proofs, then scans. Set function: to verify one target, args: for -I/-D/--link/--unwind.

On an existing codebase, record what is already there first — otherwise the first run fails on everything it finds and the check gets removed:

veripp accept src/ --baseline .veripp-baseline   # commit this

name: verify
on: [pull_request]

permissions:
  contents: read
  security-events: write      # required to upload SARIF

jobs:
  veripp:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - uses: gfabbretti8/veripp@main
        id: verify
        continue-on-error: true    # let the SARIF upload run either way
        with:
          source: src/
          baseline: .veripp-baseline
          sarif: veripp.sarif

      - uses: github/codeql-action/upload-sarif@v3
        if: always()
        with:
          sarif_file: veripp.sarif

      - name: Fail on new findings
        if: steps.verify.outcome == 'failure'
        run: exit 1

continue-on-error plus the explicit final step is deliberate: without it a finding fails the job before the SARIF is uploaded, and the annotations that explain the failure never appear on the diff.

With sarif: each finding becomes an annotation on the pull request diff instead of a line in a job log. Findings covered by the baseline are uploaded as suppressed rather than omitted, so code scanning shows them as accepted rather than pretending they are gone.

Now the job goes red only on findings that are not in the baseline. The file is JSON and meant to be reviewed in the pull request that adds it: each entry is a risk somebody decided to carry. When a finding stops occurring, veripp says so, because an entry that matches nothing still grants permission to whatever matches it later.

fail-on: never remains for a first look, but a check that can never fail is a check nobody reads.

In a container

docker run --rm -v "$PWD:/src" ghcr.io/gfabbretti8/veripp scan src/parser.c

Nothing to install, and the checker inside has already been probed: the image build runs veripp doctor and fails if the bundled ESBMC cannot find a planted bug, so an unsound image is never published.

The image is genuinely multi-architecture, and the two halves are not built the same way. ESBMC publishes a prebuilt Linux binary for x86_64 only. The one prebuilt arm64 Linux ESBMC that exists anywhere is the Homebrew bottle, pinned to the 8.4 release that silently misses out-of-bounds writes (esbmc#6508) — shipping that would trade a loud failure for a quiet one. So the arm64 image compiles ESBMC from source, and arm64 users get the same soundness guarantee as everyone else.

The container runs as a non-root user and never writes to your tree, so the mount can be read-only:

docker run --rm -v "$PWD:/src:ro" ghcr.io/gfabbretti8/veripp \
    verify src/img.c --function scale --assume 'w > 0 && h > 0'

--compile-commands works too, even though your compile_commands.json records absolute paths from your machine and the tree is mounted at /src inside. veripp finds the entry by its trailing path components and rebases the whole thing — include dirs included — onto wherever the tree actually is. The same applies to a CI checkout that does not sit where the database was generated. If two entries match equally well it says so rather than guess.

The container runs as a non-root user, which means it cannot read a project directory that is not readable by others — a tree under a 0700 home directory, typically. If /src comes up unreadable, veripp says so and you can run as yourself instead:

docker run --rm --user "$(id -u):$(id -g)" -v "$PWD:/src:ro" \
    ghcr.io/gfabbretti8/veripp scan src/parser.c

Roughly 450 MB (amd64) and 530 MB (arm64), most of it ESBMC itself.

Repeat runs are cached

A second scan reuses verdicts for files that have not changed, which is what makes this affordable on every push rather than nightly. The key covers the file, the local headers it includes, any linked sources, the bounds, the harness options and the checker's own version — so a stale verdict cannot be served. --no-cache verifies everything; --cache DIR moves it.

Deliberately not keyed on the function body, which would be unsound:

static int limit(void) { return 4; }
int at(const int *a, int i) { if (i<0 || i>=limit()) return 0; return a[i]; }

at verifies. Change limit to return 99 and at — byte-identical — yields a counterexample.

As a skill for coding agents

The quickest way, needing nothing but Node:

npx veripp-skill            # this project
npx veripp-skill --global   # every project

That installs the skill only. The verifier is a Python program that needs ESBMC; the skill carries a script that works out how to get it and reports what that would cost before touching anything.

In Claude Code you can also install it as a plugin from this repository:

/plugin marketplace add gfabbretti8/veripp
/plugin install veripp@veripp

For any other agent, copy skills/veripp wherever it keeps skills. Either way the agent will reach for veripp when it is asked to verify or prove something about C/C++.

The skill exists to correct one specific instinct. An agent that knows ESBMC will try to hand-write a main() full of __ESBMC_nondet_int(), sprinkle __ESBMC_assume(...), and annotate loops with invariants. veripp already generates all of that from the signature, and re-checks it. The skill's first instruction is that the agent does not write the harness — plus how to read a bounded proof, and why a vacuous result is not a pass.

Scan a whole project

veripp scan src/            # every .c/.cc/.cpp/.cxx underneath
veripp scan . --jobs 8
veripp scan src/ --only 'parse_*'   # just the ones you are working on
veripp scan src/                    # unchanged files are reused from cache

Build trees, vendored dependencies and dotted directories are skipped (build/, node_modules/, third_party/, .git/, ...), and headers are left alone because definitions live in the source file. The file count is printed before the work starts, findings are grouped by file, and the exit code is 1 if anything anywhere failed.

Adding veripp to code that already exists

The first run on an existing codebase reports everything at once — cJSON gives 33 counterexamples. Record what is already there, then fail only on what appears afterwards:

veripp accept src/ --baseline .veripp-baseline   # commit this
veripp scan   src/ --baseline .veripp-baseline   # exits 1 only on new findings

The file is JSON, sorted, and meant to be reviewed in the pull request that adds it: each entry is a risk someone decided to carry, with the signature and the date recorded beside it. Findings are keyed on (file, function, property) rather than line numbers, so moving code around does not resurrect an accepted finding. When one stops occurring veripp says so, because an entry that matches nothing still grants permission to whatever matches it later.

Scan a whole file

veripp scan src/parser.cpp

Harnesses and verifies every function veripp can model, then reports what it proved, what produced counterexamples, and — importantly — what it could not reach and why:

  PROVED             99  no overflow, out-of-bounds, null deref or division by
                         zero, within the stated bounds and assumptions
  COUNTEREXAMPLE     61  a property fails for some input -- triage each one
  HARNESS ARTIFACT    3  failed because of how the harness was built, not the code
  INCONCLUSIVE       52  timed out, hit the unwind bound, or the frontend refused it
  NOT HARNESSABLE    47  veripp could not build inputs for the signature

(That is real output from veripp scan on lodepng.cpp.)

--json for machine-readable output, -j for parallelism.

Real projects

veripp reads your build system rather than making you restate it. Point it at a source file and it finds the nearest compile_commands.json (including in build/), and takes that file's include paths, defines and language standard from it:

veripp verify src/area.cpp --function area
# note: using build/compile_commands.json (1 include dirs, 1 defines, -std=c++17)

Use --compile-commands PATH to choose one, --no-compile-commands to ignore them.

Linking matters for soundness, not convenience. ESBMC gives an undefined function a nondeterministic return value, but assumes it does not write through its pointer arguments. So a callee whose definition is in another translation unit is silently treated as side-effect-free. veripp detects those callees itself — ESBMC reports them for C but not for C++ — and names them:

STUBBED CALLS (no body was available): normalize. Their effects were not
modelled, so this counterexample may be an artifact of the missing definition
rather than a real bug -- check it first.

Add the defining source with --link src/helper.cpp (repeatable) and the run accounts for it. In the example above that is the difference between a false counterexample and a proof.

Vacuous proofs

A precondition that cannot be satisfied makes the target unreachable, and an unreachable program satisfies every property. ESBMC answers "does this hold under these assumptions" — it cannot notice the assumptions are impossible, and neither can a model that proposed them. Since the whole design lets an LLM suggest preconditions, that hole matters: a weak model fails toward over-constraining, and the solver applauds.

So whenever a proof rests on assumptions, veripp re-runs the harness with a deliberately false assertion at the end. A reachable harness must fail it; if it verifies instead, nothing was checked:

Result: VACUOUS (nothing was actually checked)
  The assumptions made the call unreachable, so every property held trivially.
  This is NOT a proof. Weaken the precondition(s) below until the harness can run.

It exits non-zero, so a vacuous proof can never pass CI.

Check your checker

veripp doctor

runs known-failing programs through your ESBMC and confirms it rejects them. A model checker that answers "verified" on a program that provably fails is worse than none, because every result built on it is a false proof. ESBMC 8.4 has one such hole (esbmc#6508, fixed upstream but unreleased): an out-of-bounds write to a member array is missed when the index is another member of the same object reached through this or a pointer — the ordinary container idiom. doctor fails loudly rather than letting you build proofs on it.

Honest-reporting policy

Every "VERIFIED" result states its unwind bounds, stubbed calls, and harness assumptions. Bounded results are labeled bounded. Overclaiming is how verification tools lose trust permanently; we don't.

Two places this bites in practice, both handled explicitly:

• ESBMC reports an exhausted unwind bound as VERIFICATION FAILED with an "unwinding assertion" property. That means the bound was too small, not your code is broken. veripp classifies it as inconclusive and widens the bound instead of reporting a bug.
• A generated harness always simplifies something — a bounded array length, a default-constructed receiver, a non-null pointer. Every such simplification is recorded and printed with the result. When the generator cannot model a parameter soundly it refuses to emit a harness rather than emit a plausible-looking wrong one.

Known limits

Read this before judging the output.

• Counterexamples need triage; not all are bugs. Where an object has no initialiser to build it from, the harness gives it every possible field value, including combinations no caller can construct — so it can report a failure that cannot happen in your program. veripp filters the mechanically decidable cases into a separate "harness artifact" count, but the rest are leads, not findings. The proofs are the trustworthy half. Use --assume (or an LLM) to state what real callers guarantee.
• The released ESBMC is unsound for a common pattern. v8.4 misses out-of-bounds writes to a member array indexed by another member of the same object (esbmc#6508, fixed upstream, unreleased). veripp doctor detects it and every affected result says so. Use a master or weekly build.
• C and C-like C++ only. ESBMC's C++ frontend does not digest STL-heavy code; tinyxml2 crashes it and jsoncpp will not parse. Codecs, parsers and embedded-style code work well.
• How much of a file veripp can reach varies. lodepng 82%, cJSON 89%, parson 91%, tinyexpr 96%. Types whose definition is not in the translation unit cannot be constructed, and those functions are refused with the reason given. Run veripp scan on your own code to find out.
• Bounded by default. A proof covers executions within the unwind bound, which is stated with every result.

Contributing

See CONTRIBUTING.md. The short version: the LLM proposes, the solver disposes, and every result states what it assumed.

License

Apache-2.0