Ecne
Direct answerEcne was the first widely used tool for proving that an R1CS constraint set uniquely determines its outputs, the property later automated with SMT by Picus. It remains useful as a lightweight second opinion on small R1CS systems.
- Maintainer
- Franklyn Wang (0xPARC)
- Website
- https://github.com/franklynwang/EcneProject
- Repository
- https://github.com/franklynwang/EcneProject
- Category
- ZK circuit verification
- Targets
- R1CS
- Approach
- Rule-based propagation to prove output uniqueness of R1CS constraint sets
- Access
- Open source (GPL-3.0)
- Status (2026-09-13)
- Low activity research tool
What Ecne does
Ecne propagates uniqueness through constraints with a set of rules rather than a solver, so it is fast but incomplete: a failure to prove uniqueness is not a bug report.
Where it is strong
- Simple, fast, historically significant.
- Works directly on R1CS output of any compiler.
Limits and caveats
- Incomplete rule set; many false negatives.
- Julia dependency; little maintenance.
- No functional properties.
When to choose it
Only as a cross-check; prefer Picus or CIVER.
Who works with Ecne
No firm on this index lists Ecne as a core tool yet; the firms below cover the same problem class.
Top-listed for circuit verification work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Related frameworks in ZK circuit verification
Clean, sp1-lean, zkLean, Halva, Picus, LLZK, Garden, Lampe, proven-zk and gnark-lean-extractor, CIVER, Circomspect, zkFuzz, Coda, NAVe, Verified Cairo AIR (Stone and S-two).