Noir analysis capability built on formal verification expertise.
For zero-knowledge applications built with Noir.
Why ZK programs need formal analysis
Zero-knowledge proofs are only as sound as the programs generating them. A ZK proof system can accept an invalid proof if the underlying circuit has a soundness bug, a vulnerability that standard security tooling simply is not built to catch.
Formal reasoning is not optional here. It is the only reliable methodology for finding constraint-level bugs: under-constrained witnesses, unsound encodings, and proof system assumptions that do not hold under adversarial conditions.
NAVe
Our Noir program analysis capability is grounded in NAVe, our open-source formal verifier for Noir zero-knowledge programs. NAVe formalises ACIR (Noir's intermediate representation) using SMT-LIB and the theory of finite fields, then verifies programs using the cvc5 SMT solver.
What we cover
- Formalisation and analysis of requirements
- Safe usage of unconstrained functions
- Constraint soundness and completeness
- Encoding correctness against intended computation
- Proof system assumptions and trusted setup review
- Verifier integration and public input binding validation
How an engagement works
Scoping
We define the circuit, proof system, and threat model in scope.
Analysis
NAVe-assisted formal analysis combined with expert manual review.
Report
Severity-graded findings with remediation guidance.
Remediation review
We verify fixes and issue a final report.
Request a ZK / Noir audit
Tell us about your circuit, proof system, and timeline. We will get back to you within one business day.