I build static analysis tools that find soundness bugs in zero-knowledge circuits — the class of bug where a prover-controlled value never gets bound to the fact it’s supposed to represent, so the proof system faithfully proves the wrong statement.

Three open-source tools, three proof systems:

o1js-scan — soundness linter for o1js / Mina zkApps and Noir circuits. Listed under community packages in the official o1js repository. Python, published to PyPI and npm.

gnark-safety — static analyzer for gnark circuits. Type-aware Go analysis, shipping as a CLI, a go vet tool, a pre-commit hook, and a GitHub Action.

vk-guard — CI guard that snapshots verification keys and constraint counts and fails the build on unexpected drift, catching changes that would break already-deployed applications.

What I actually spend my time on is calibration rather than rule count. Every rule set runs against large bodies of reviewed production code with each finding read and classified in a committed public record. A high-severity false positive means the rule gets fixed, not filed as an exception. Every suppression ships with a paired test proving the rule still fires when the safety property is removed — because a rule that has learned to stay quiet looks identical to one that has learned to discriminate.

I also write about vulnerability taxonomy and false-positive analysis. The recurring theme: a clean run means no pattern these rules recognize matched, not that the code is safe, and a tool that blurs that distinction is worse than no tool.

github.com/auditinfra-io