A proof that verifies is not the same thing as a circuit that proves what you think it does. Groth16 and PLONK verifiers are small, well-reviewed pieces of arithmetic; the bugs that drain value live in the gap between the statement the developer meant to prove and the statement the constraints actually enforce. Auditing a ZK smart contract means checking three systems that fail independently: the circuit, the setup that produced its keys, and the Solidity that consumes the proof. Work through them in that order and you will catch most of what matters.
Write the relation in plain English first. What does a valid proof claim? Which signals are public inputs, in what order, and with what bit widths? Who is allowed to generate a proof, and what stops one from being reused? If there is no spec in the repository that answers these questions, that is finding number one.
Then ask the adversarial version: the proving key is public, so an attacker has it. What could they prove that the application does not want them to prove? A membership circuit that lets a prover choose the Merkle path directions freely will happily accept a proof for a leaf that was never inserted. The verifier cannot see that. Only the constraint set can prevent it.
Most circuit vulnerabilities are constraint bugs, not math bugs. Read every hint assignment and ask what forces the witness to take the value you expect.
In Circom, writing out <-- a / b computes a witness value and adds no constraint at all. You also need out * b === a, plus a check that b is nonzero. The <== operator is the constrained form. Search the codebase for every <-- and justify each one in writing.
A field element is not a uint64. Wherever a value is later interpreted as an integer, enforce its bit width with a decomposition gadget such as Num2Bits, then check that the recomposed value equals the original. Comparisons on raw field elements are meaningless without a range bound.
Two signals that should be distinct are often linked only by an equality the prover can satisfy in more than one way. Trace each public input through to every constraint that touches it, and confirm there is exactly one intended assignment.
The prover's JavaScript or Rust code computes the witness. If it orders, hashes, or endian-swaps inputs differently from the verifier, you get failed proofs at best and valid proofs for the wrong statement at worst. Reimplement the witness derivation independently and diff the outputs on the same inputs.
Groth16 needs a per-circuit phase 2 ceremony. If any single participant kept their randomness, they can forge proofs for false statements, and nothing on-chain reveals it. Check the transcript: the powers-of-tau hash, the list of contributions, and the public beacon at the end. Then confirm the verifying key embedded in the deployed contract matches the key that ceremony produced, by hashing the key file in the repo and comparing.
The subtler failure is a circuit edited after the ceremony finished. Adding a public input, reordering signals, or changing a constant invalidates the setup, yet the old verifying key still accepts proofs for the old relation. Pin the circuit commit hash and treat any change as requiring a fresh phase 2.
Transparent systems — STARKs, Halo2, Bulletproofs — remove this class of risk entirely, at a cost in proof size or verification gas. That trade-off belongs in the report, not in a footnote.
Assume the pairing check is correct, then look at everything around it.
Build a negative test for every public input: flip one bit and expect rejection. Fuzz the witness generator with edge values — zero, one, and the field modulus minus one. Compare the circuit against a second, independent implementation of the same relation, even a slow Python one. Constraint-level property tests and symbolic tools catch under-constrained signals that manual review misses. Mutation testing helps too: change a constraint and confirm at least one test fails.
Record the exact commit, artifact hashes, and ceremony transcript the audit covers, and publish the verifying key hash so users can check the deployed contract themselves. Require a regression test for every finding, and re-run the relevant parts of this checklist after any circuit change — a one-line edit can invalidate a setup or loosen a constraint. Zero-knowledge systems reward that kind of bookkeeping. The cryptography will hold. The constraints are where you earn your keep.
Photo: HarinathR / Pixabay
