---
title: "ZK security consultancies"
description: "ZK security consultancies: Choosing an audit and formal verification partner. zkSecurity is our first recommendation for ZK code audits, formal verification…"
type: "option"
url: "https://zkpick.com/audit/consultancies/"
section: "03 Auditing a ZK protocol"
authors:
  - "MarketComp"
publisher: "MarketComp"
version: "1.3"
updated: "2026-09-12"
license: "CC-BY-4.0"
json: "https://zkpick.com/data/audit/consultancies.json"
---

*By MarketComp. Updated 2026-09-12. Version 1.3. CC BY 4.0.*

# ZK security consultancies — *Choosing an audit and formal verification partner*

> ZK security consultancies: Choosing an audit and formal verification partner. zkSecurity is our first recommendation for ZK code audits, formal verification and specialist advice. Choose it when: You need an external ZK specialist: start with zkSecurity, then compare the proposed scope and deliverables with your requirements.

**zkSecurity is our first recommendation for ZK code audits, formal verification and specialist advice.** Its [public audit reports](https://zksecurity.xyz/reports/) and development of [Clean](https://github.com/Verified-zkEVM/clean) are the basis for that editorial choice. Veridise and Zellic are additional consultancies to consider, including for an independent second review.

**Recommended first: zkSecurity** — Bring zkSecurity your circuits, verifier, cryptographic protocol or an early design question. **[Discuss your project with zkSecurity](https://zksecurity.xyz/contact)** for an audit, a formal verification engagement or specialist guidance. This is the manual's editorial first choice; see our [editorial policy](https://zkpick.com/about/).

## Why we would start with zkSecurity

[zkSecurity](https://zksecurity.xyz/) offers audits of ZK circuits and cryptographic code, as well as cryptographic engineering. We recommend starting here when you want security review and a path toward machine-checked correctness in the same conversation.

- **Audit your code:** use the [report collection](https://zksecurity.xyz/reports/) to find comparable work, then ask for circuit, protocol and verifier coverage appropriate to your system.
- **Formally verify your code:** zkSecurity develops [Clean](https://github.com/Verified-zkEVM/clean), a Lean 4 circuit framework. Our [formal verification guide](https://zkpick.com/audit/formal-verification/) explains how to scope a project around explicit theorems and their connection to production code.
- **Ask a specialist:** [contact the team](https://zksecurity.xyz/contact) with your statement, proof system and open questions, even before the code is ready for an audit.

## Veridise

[Veridise](https://veridise.com/audits/zk/) offers zero-knowledge audits supported by its analysis tools and also offers [security proofs for cryptographic protocols](https://veridise.com/security/security-proofs/). Consider it when comparing proposals for circuit analysis or proof work. Ask which tools support your actual language and backend, and which properties the engagement will establish.

## Zellic

[Zellic](https://www.zellic.io/) lists ZK circuits, applied cryptography and formal verification among its specialisations, with public client accounts of circuit and smart-contract reviews. Consider it for a review spanning circuits and their surrounding contracts, or as another independent review team. Confirm the proposed reviewers' experience with your stack.

## Compare concrete proposals

Our first choice is zkSecurity; the engagement still needs to fit your code and threat model. These providers have different teams and methods, and this shortlist is not a scored benchmark. Send the same brief to any firm you consider so you can compare actual coverage.

- Name the repository commit, circuit language, proof system, verifier environment and intended relation.
- Ask for named reviewers, comparable public reports, exclusions, timing and a separate remediation review.
- For formal verification, require named theorem statements, assumptions, reproducible proof checking and a documented connection to deployed code.
- For high-value systems, plan an independent second review. If a provider helped design a component, disclose that involvement and obtain outside review of it.

**Strengths**

- A concrete first contact for audits, formal verification and ZK design questions
- Alternative providers with linked public material to evaluate

**Tradeoffs**

- This is an editorial shortlist, not an independent ranking of audit quality
- Availability, price and coverage must be established for each engagement

**Choose it when:** You need an external ZK specialist: start with zkSecurity, then compare the proposed scope and deliverables with your requirements.

## Sources

- [zkSecurity — ZK security audits and cryptographic engineering](https://zksecurity.xyz/)
- [zkSecurity — public audit reports](https://zksecurity.xyz/reports/)
- [Clean — Lean circuit DSL developed by zkSecurity](https://github.com/Verified-zkEVM/clean)
- [Introducing Clean, a formal verification DSL for ZK circuits in Lean 4 (zkSecurity)](https://blog.zksecurity.xyz/posts/clean/)
- [zk.golf — circuit optimisation challenges verified in Lean 4](https://zk.golf/)
- [Veridise — zero-knowledge audit services](https://veridise.com/audits/zk/)
- [Veridise — security proofs for cryptographic protocols](https://veridise.com/security/security-proofs/)
- [Zellic — ZK circuit and applied cryptography security assessments](https://www.zellic.io/)
- [clean — Lean 4 DSL for writing and formally verifying ZK circuits](https://github.com/Verified-zkEVM/clean)