> ## Documentation Index
> Fetch the complete documentation index at: https://docs.graphify.com/llms.txt
> Use this file to discover all available pages before exploring further.
# Differential verification
> Understand the enterprise verification workflow and what each verdict means.
Graphify’s website describes **differential formal verification** in the enterprise distribution. It compares supported changed functions with their previous versions. The old implementation acts as the behavioral reference.
This is an enterprise capability. The commands below require that distribution; they are not part of the public `graphifyy` CLI audited for these docs. [Request enterprise access](https://graphify.com/enterprise/access).
## Read the verdict
| Verdict | Meaning |
| ---------------- | ------------------------------------------------------------------------------------- |
| `equivalent` | The selected proof method established equivalence in its supported domain or bounds. |
| `distinguished` | A concrete input distinguishes the two implementations. |
| `may_equivalent` | Exercised inputs did not show a difference. This is empirical agreement, not a proof. |
| `unsupported` | The method abstained, with a reason. |
| `error` | Infrastructure failed to produce a valid verdict. |
## How the tiers fit together
The documented enterprise ladder uses symbolic proof where supported, then methods such as concolic execution, property-based comparison, and replay of arguments captured from tests. Tiers that execute code require enforced sandbox isolation.
Python proof tiers cover supported function fragments. C, C++, and Java proof results are bounded by the configured analysis. Other language paths may offer empirical comparisons or abstain. Confirm the exact support of your installed enterprise release.
## Enterprise command examples
```bash theme={null}
graphify verify-edit compute_total --base HEAD~1 --emit-test test_regress.py
graphify gate --verify-edits --base origin/main --carve --block-behavior-change
```
These examples come from the existing [Graphify verification guide](https://graphify.com/docs/verification). The gate’s blocking behavior is explicit in the second command.
## Limits
Function-level equivalence does not prove the application meets its intended requirements. A bounded proof applies only within its analyzed bounds. Timeouts, unsupported inputs, and missing isolation should remain visible as abstentions or failures; they must not be interpreted as successful verification.
Use graph context, tests, review, and verification as complementary evidence.