Case study
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.
- Client
- Unlink
- Verified guarantees
- 4
- Date
- May 2026
Overview
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.
Why formal verification
Why Unlink chose formal verification over a classic audit
A classic security audit is valuable for finding bugs and attack paths, but it cannot guarantee that no bug remains. Formal verification takes the next step: under a defined set of specifications and assumptions, it provides a mathematical guarantee that the verified properties hold and that no bug violating those properties remains in the modeled system.
That assurance also makes maintenance more efficient. For any upgrade that preserves the verified invariants, we re-prove those invariants during the maintenance window at no extra cost. Because qualifying upgrades do not require a separate re-audit fee, formal verification becomes more economical to maintain over time.
With that standard of assurance in mind, Unlink chose Verity because we combine deep formal-methods expertise with AI-first Lean workflows developed with support from the Ethereum Foundation. This makes us particularly well suited to proving Solidity systems with complex mathematical and contract-level behavior, while the efficiency of an AI-native firm keeps the work practical and cost-effective for teams like Unlink.
Testimonial
Verity’s formal audit gave us a clear understanding of what the system depends on, and which dependencies we need to monitor while formal verification proved what the code guarantees. Together, that gives us much stronger confidence in our code and a solid foundation for shipping Unlink.
Key findings
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
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.
Contact our team
We take 4 protocols per quarter. Formal verification demands deep focus. We'd rather verify fewer contracts well than many poorly.
Continue reading
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.