Skip to main content
Stop guessing which inputs to test. Formal verification uses math to show code behaves a certain way for every input in scope, not just the ones you tested. When it can’t, a good verifier gives you an input that breaks the claim.

​
Tests sample. Reviews judge. Proofs cover.

Say you change a function that rounds prices. Use all three. Tests document intent, reviews catch design problems, and proofs cover cases nobody thought of.

​
Prove against what you already have

Write a spec

A written rule, like “the result is never negative”. Takes work, and most codebases don’t have one.

Reuse the previous version

“New returns the same as old for every input.” Called equivalence checking. Needs no spec. Graphify uses this.
It fits refactors, performance work and agent-written code. The catch: if the old code had a bug, an equivalent new version has it too.

​
Know where a proof stops

Verifiers limit input size, language features or time. A bounded proof holds within those limits, so there are more answers than pass and fail: Graphify reports each one separately. It never turns “couldn’t decide” into a pass.

​
Turn a counterexample into a test

The distinguishing input gives you the exact arguments plus the old and new results. Use it to:
1

Reproduce

Run both versions on it.
2

Decide

Was the change intended, like a bug fix?
3

Pin it

Turn it into a regression test.

​
In Graphify

Each pull request gets an advisory Graphify Formal Verification check on GitHub. It never blocks a merge.

Formal verification

How the check works and supported languages.

Read a review and a verdict

Review findings vs verification verdicts.