Prove a change is safe, or get the exact input that breaks it.
Graphify Enterprise runs differential formal verification on every pull request. No specs to write: the old code is the spec. For each changed function, a solver looks for an input where the new version behaves differently. If none can exist, the change is proven behavior-preserving. If one does, you get the concrete distinguishing input.
❌ apply_discount [smt] · behavior changed. Distinguishing input: (price=100, qty=1) → old=100, new=90.def test_apply_discount_preserves_behavior(): # distinguishing input found by differential verification; # OLD returned 100, NEW returned 90 assert apply_discount(100, 1) == 100When behavior changed, you get the exact input that shows it, and, for Python and JavaScript, a ready-to-commit regression test that pins the old behavior. C, C++, Java, and Go emit a comment-form pin instead.
Four verdicts, never a bluff.
A checkmark you can't audit is worse than no checkmark. Every run lands on exactly one verdict, and says which and why. (A fifth state,error, reports infrastructure failures rather than turning them into a verdict.)
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.
Proofs are unbounded for Python. For C, C++, and Java the solver is bit-precise but bounded(loops unwound, object depth capped), so "equivalent" there means proven within the analyzed bounds; a blown bound is downgraded to "no divergence found," never a false proof.
It only answers when it actually knows.
Verification reasons about the code with a solver, not a model, so a pass means proved, not "looked fine to an LLM." The integrity is enforced, not promised:
Proofs must bite
A proof over a domain no input can reach is refused and downgraded to an abstain. No vacuous green checks.
Statistics are labeled
Agreement over sampled inputs is always marked “no divergence found, not a proof,” never dressed up as sound.
Counterexamples are replayed
Every solver-found breaking input is re-run in a sandbox before it counts, so a modeling artifact is never presented as a real bug.
Unsupported over guessing
When Graphify can’t decide, it says so, with the reason. It never emits a guessed verdict.
On every pull request, automatically.
The self-hosted Graphify GitHub App verifies changed functions on each PR and posts the results into the check, advisory by default, and a hard block only when you turn enforcement on. A coverage nudge even points at the changed functions that are one test away from becoming verifiable.
Your code never leaves the machine.
The solvers (Z3, CBMC, JBMC) run locally; the executing tiers run in a network-denied sandbox; fork PRs are never run without an explicit opt-in. There is no LLM and no network call anywhere in the verification path.
Measured, not promised.
Languages today
Sound proof tiers for Python and, within analyzed bounds, C, C++, and Java. Property-based differential testing for Go and JavaScript. Rust and TypeScript changes are tracked in the code graph but not verified today.
We publish our abstain rate
On arbitrary historical changes, most functions honestly abstain (about 1% get a decisive verdict with no repo context, rising to roughly 17 to 45% with the repo's own test suite). The bottleneck is input construction, not proof power, which is exactly what trace-carving and the coverage nudge address. In our benchmark, letting the verifier decide equivalence instead of an LLM cut verification tokens by about 92%.
Available today in self-hosted Graphify Enterprise.
It ships in the self-hosted enterprise distribution and is in early access with design partners. The open-source core (the on-device graph and query) is free and live today. If proving behavior on every change is something your team needs, tell us how you ship and we'll scope the deployment.
Try it on your own repo.
93,830 stars on GitHub. Read the code.Evaluating for a team? See Graphify Enterprise →