CirC still seems like the more usable bridge for most teams, since it keeps you closer to SMT and compiler-ish IRs, while zkPi is aimed at the nicer story of proving Lean theorems themselves. The tradeoff is that Lean buys you a much stronger statement about the spec, but you pay for it in proof effort and in the gap between the theorem and the thing a non-math reviewer can eyeball.

I keep wondering whether the bottleneck is proof generation or just getting Lean's kernel assumptions into a ZK-friendly shape.