Pre-audit
A pre-audit before the paid audit.
Find the cheap, mechanical bugs first, so your auditors spend their hours on the hard ones.
The pipeline
Five steps, each leaves an artifact.
- ScopeCircuits, prover, spec.artifact: scope note
- Automated passMinutes, not days.artifact: raw results
- Expert reviewWhere the hours go.artifact: triaged findings
- ReportReplayable evidence.artifact: AUDIT.md (sample)
- Fix verificationOne round.artifact: closed / open list
Automated checks
What the toolkit runs.
- Spec-conformance. Labelled accept and reject vectors run through the real prover. A reject vector that is accepted is a missing constraint.
- Determinism. Identical inputs must give identical outputs.
- Proof and verifier integrity. A valid witness verifies; a tampered proof does not.
- Source lint. Unconstrained or
unsafecode, unenforced predicates, narrowing casts, division, constraint density. - Formal checks (optional, Circom). Uniqueness, range, binding and division-by-zero checks with an SMT solver, with a per-check time limit; a timeout is not counted as a detection.
Manual review
What stays human.
- Constraint-system review for under-determined outputs.
- Nullifier and commitment derivation, domain separation, replay.
- Trusted-setup and proof-system parameters where they apply.
- On-chain verifier integration: public-input encoding, output checks, nullifier registry.
Honest boundary: the automated pass is only as good as the vectors and the lint heuristics. It does not replace a full audit and gives no guarantee of absence of defects.