Skip to main content
Graphify Cloud includes Formal Verification as a core feature. It compares changed functions with their earlier implementations to determine whether behavior is preserved or whether a concrete input produces a different result. Open Formal Verification in Graphify Cloud. Hosted plans include verification with different usage and concurrency allowances; see current plans.

Inspect a verification run

1

Choose the repository

Use the Repository filter or select All repositories to see workspace runs.
2

Open a run

Check the pull request and commit, then expand the run to inspect its outcome and per-function results. A finished run can contain a mixture of outcomes.
3

Follow the evidence

Inspect the source file, function, and verdict. For a behavior change, the detail can include the distinguishing input and the old and new values. An abstention or failure includes its reason when available.
4

Return to the change

Use Open pull request or the commit link to investigate the implementation. When a run has finished, Re-run verification can queue another attempt; queued and running attempts cannot be rerun simultaneously.

Understand the result

Completed describes a run’s lifecycle; it does not mean every function was proved equivalent. Queued, verifying, failed, cancelled, skipped, and expired runs also retain their own status. A run that verified no functions does not imply the change passed.

Configure and use verification

Repository controls include a Formal verification setting for pull requests. Use Repositories and builds to check repository configuration and indexing before investigating missing runs. When Graphify supplies a distinguishing input, use it to reproduce the difference and create a regression test. Review whether the changed behavior was intentional before deciding what to change. Learning tunes advisory review feedback only. It cannot change proof verdicts or hide a witness from the verifier.

Scope of a proof

Verification is function-level and differential: the previous implementation is the reference. It does not establish that the application meets its intended requirements. Read bounds, unsupported cases, and reproduction status with the result. For the separately installed enterprise CLI, the website’s verification reference documents verify-edit and gate configuration. Those commands are distinct from the hosted console workflow and the public open-source CLI.