Skip to content
Graphify
Get started
Docs · Verification

Formal verification, explained.

Differential verification · Z3 · CBMC · JBMC

Graphify Enterprise ships differential formal verification (internally, verify-edit): for each changed function, it decides whether the new version is observationally equivalent to the old one, or finds a distinguishing input. The old code is the spec; you write nothing. This is the enterprise layer; the open-source core (graph and query) is free and on-device. For the overview, see the formal verification page.

Verdicts

  • equivalent

    01/04

    Proved behavior-preserving over all inputs. Sound. (Z3 · CBMC · JBMC)

  • distinguished

    02/04

    Behavior changed. Here’s the exact input, and a regression test ready to commit.

  • may_equivalent

    03/04

    No divergence found. Empirical, not a proof, and we say so.

  • unsupported

    04/04

    We couldn’t reach it. We tell you that, instead of guessing.

  • equivalent proves no input distinguishes old and new. Sound (unbounded for Python; bounded for C/C++/Java, see limits). A proof over a domain no input reaches is refused as vacuous.
  • distinguished gives a concrete witness input with both the old and new outputs. Sound: solver-proved, or actually executed.
  • may_equivalent found no divergence over the exercised inputs. Empirical, not a proof, and the check says so every time.
  • unsupported is an honest abstain, with the reason.

An error state exists for infrastructure failures (e.g. a harness that produced no verdict); it is reported, never converted into a verdict. Solver-found counterexamples are replayed in the sandbox first: a witness that does not reproduce at runtime is labeled a likely false alarm and excluded from the behavior-changed count.

The tier ladder

Each tier runs only when everything above it abstained:

  1. SMT (Z3): sound equivalence or refutation over all inputs, for pure Python functions over int/bool/str/float/lists of scalars.
  2. Loop-invariant tier: sound equivalent for single-loop pure Int/Bool functions via Z3-checked coupling invariants (proof-only, never refutes).
  3. CrossHair (concolic): sound counterexamples by symbolic execution of the real code; inconclusive results fall through.
  4. Property tier: both versions executed on a deterministic input corpus in a network-denied sandbox; a divergence is a sound refutation, agreement is may_equivalent.
  5. Trace-carving: captures real receivers and arguments from your own pytest suite and replays them against both versions; this is how methods and framework objects (the dominant abstain cause) get verified.
  6. Honest abstain.

Tiers 3 to 5 execute code, so they run only when sandbox isolation is actually in force (seatbelt / bubblewrap / docker, all with networking denied). Without isolation they are skipped and the pipeline abstains; it never executes PR code unsandboxed.

Languages

  • Python: Z3 SMT and loop-invariant tiers (plus CrossHair counterexamples), then property and trace-carving.
  • C / C++: CBMC (bit-precise, bounded), property fallback.
  • Java: JBMC (bit-precise, bounded), property fallback.
  • Go, JavaScript: property tier only (no sound proof).
  • Rust, TypeScript, everything else: not verified today; tracked in the graph, honest abstain.

Running it

CLI

terminal
# one function: working tree vs git base; exit 1 iff behavior changed$ graphify verify-edit compute_total --base HEAD~1 --emit-test test_regress.py # opt-in deeper tiers$ graphify verify-edit compute_total --crosshair --carve-tests tests/ # whole change set as a CI gate (advisory unless --block-behavior-change)$ graphify gate --verify-edits --base origin/main --carve --block-behavior-change

Prerequisites: a built graph (graphify build), a git checkout, and z3-solver. Optional: cbmc, jbmc + JDK, go, node, crosshair-tool; a missing tool means that tier abstains, and startup validation warns you. graphify verify-plan <fn> prints the blast radius and the callee-first re-verification order for a change.

GitHub App

With the self-hosted app installed, verification runs on every PR by default and posts a graphify verify-edit section in the Graphify check: headline counts, per-function verdicts, evidence tiers for behavior changes (confirmed / hypothesis / likely-false-alarm, with the public caller path), the suggested regression test, and a coverage-gap nudge listing changed functions that are one test away from verifiability. Key knobs:

  • GRAPHIFY_ENT_VERIFY_EDITS (default on) runs verify-edit on PRs.
  • GRAPHIFY_ENT_BLOCK_BEHAVIOR_CHANGE (default off) makes a behavior-changed edit fail the check. Verification is advisory until you set this.
  • GRAPHIFY_ENT_MAX_VERIFY_FNS and GRAPHIFY_ENT_VERIFY_BUDGET_S cap work per PR (both configurable); any truncation is annotated in the check, never silent.
  • GRAPHIFY_ENT_ISOLATION (auto) selects the sandbox backend; GRAPHIFY_ENT_VERIFY_FORKS (off) keeps fork PR code from ever running unless opted in.

Limits (read this)

  • Function-level and differential.It compares one changed function's two versions; cross-function and heap-interaction effects are out of scope. It proves a change is behavior-preserving, not that the code is correct against intent.
  • C/C++/Java proofs are bounded(loops are unwound to a configured depth and object/array synthesis is depth-limited): "equivalent" there means within the analyzed bounds; blown bounds downgrade to may_equivalent, never a silent proof.
  • Abstains dominate on arbitrary code. On 250 real historical changed functions with no repo context, about 1% got a decisive verdict, and 92% of abstains were input-construction failures (methods needing real objects), not proof-fragment gaps. With the full ladder in-repo (sandbox plus your test suite) we measured roughly 17 to 45% decisive on our own history. The coverage-gap nudge exists because a test that exercises a function is what unlocks its verification.
  • may_equivalent is not a proof, and the check says so every time. Solver timeouts and per-PR caps abstain or are annotated, never guessed.
  • Nothing leaves your machine: local solvers, network-denied sandboxes, no LLM in the verification path.

This runs in the self-hosted enterprise distribution, in early access. Request early accessand we'll scope the deployment. New to Graphify? Start with the quickstart and the concepts.