would a machine-checked soundness library for circomlib be useful?

[attilavjda]

While formalizing related math, AI agent suggested and built Lean4 proofs that I don't yet fully understand, but might be valuable:

• that circomlib templates (IsZero, Num2Bits, LessThan, comparators, a Poseidon S-box)
  are sound + complete + deterministic against a spec

i.e. no under-constraint (<-- without ===) and no spec↔R1CS mismatch.
Aliasing side conditions like 2^n ≤ p show up as explicit hypotheses.

repo: circomlib templates verifications

Would a verified companion library like this be useful to the ecosystem?
If so, which template(s) would you prioritize verifying first?

Thanks!