Ecne: Early R1CS uniqueness checker in Julia
============================================

Ecne 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
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: Low activity research tool
Strengths: Simple, fast, historically significant. | Works directly on R1CS output of any compiler.
Limits: Incomplete rule set; many false negatives. | Julia dependency; little maintenance. | No functional properties.
Firms using it: none listed
Sources: https://github.com/franklynwang/EcneProject

Source page: https://sorryfree.com/frameworks/ecne/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13