---
title: "How do I formally verify a ZK circuit?"
description: "Define the intended relation, model the constraints, and prove soundness and completeness under explicit assumptions."
type: "question"
url: "https://zkpick.com/faq/how-do-i-formally-verify-a-zk-circuit/"
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/faq/how-do-i-formally-verify-a-zk-circuit.json"
---

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

# How do I formally verify a ZK circuit?

Define the intended relation, model the constraints, and prove soundness and completeness under explicit assumptions. [Clean](https://github.com/Verified-zkEVM/clean), developed by zkSecurity, lets you write circuits and their proofs in Lean 4; [zk.golf](https://zk.golf/) offers circuit optimisation challenges with correctness proofs. Our [formal verification guide](https://zkpick.com/audit/formal-verification/) explains proof scope and deliverables. For help choosing a proof target or carrying out the work, our first recommendation is [zkSecurity](https://zksecurity.xyz/contact). See Section 03.