Formal Verification for Private Onchain Payments
An independent review of Unlink's contract and zero-knowledge circuit surface at commit 7617b3e (May 2026). Unlink lets applications deposit ERC-20 tokens, move value as private notes, and withdraw publicly without exposing a transfer's sender, recipient, or amount. The full report records the evidence, source crosswalk, and remediation status.
Our approach
We first run a security review audit to find where the system can fail. Once those issues are fixed, we apply formal verification: mathematically proving the corrected modeled system is fully correct against its formal specification and stated assumptions, with no covered failure modes left.
Findings summary
| Area | Result | Status |
|---|---|---|
| In scope Contract and circuit security | No scored findings. No High or Critical exploit path was identified in the audited surface. | Reviewed at the pinned source snapshot. |
| In scope ZK release engineering, CI, and tooling | 11 scored findings: four Medium and seven Low. They covered artifact identity and provenance, verifier hardening, and missing CI/test gates. | All 11 were remediated and verified resolved. |
| Out of scope Backend, SDK, dashboard, deployment, and operations | Observations were handed to the relevant workstreams, but were not scored findings and carry no audit verdict in this report. | All but two observations were verified resolved. Two remain accepted deferrals for deployment/governance and local wallet handling. |
Formal Verification Summary
| Property | Status | What it establishes |
|---|---|---|
| No double-spend | Proved | A recorded nullifier cannot be spent again. |
| Verify before mutate | Proved | Proof verification precedes state changes. |
| Merkle-root bookkeeping | Proved | A successful insertion stores the root it computed. |
| Exact token deltas | Proved | Modeled deposit and transfer token movements match exactly. |
| Cross-note value conservation | Circuit boundary | Enforced by the spend circuit, not stated over contract state. |
This protects the modeled contract rules with respect to the formal specs and assumptions written by the Verity team. Special thank you to the Unlink team for their professionalism throughout the engagement.
Learn more
Read the full audit report (PDF)
Unlink security and the Unlink trust model.
What is a formal proof? A short introduction for non-specialists.