halo2-analyzer (Korrekt)
Open SourceQuantstamp's analysis tool for detecting under-constrained halo2 circuits.
About
halo2-analyzer, also known by its research name Korrekt, is a tool from Quantstamp for finding under-constrained behavior in halo2 circuits. It extracts constraints from a halo2 circuit and checks whether the circuit admits multiple satisfying assignments for the same public inputs, which would indicate a soundness vulnerability. Halo2's custom gates and copy constraints make manual review difficult, so automated uniqueness checking is a valuable complement to audits of halo2-based systems.
Categories
Static Analysis Formal Verification
Chains
halo2