Open Issues Need Help
View All on GitHub [circomlib] Prove `Sign` soundness and completeness about 1 month ago
good first issue gadget
[circomlib] Add remaining proofs in `Bitify2` about 1 month ago
AI Summary: Implement missing proofs for the `Bits2Num_strict` and `Num2BitsNeg` functions within the `Bitify2` module of the `clean` Lean circuit DSL. This involves formal verification using Lean's theorem proving capabilities.
Complexity:
4/5
good first issue gadget
[circomlib] Add remaining proofs in `Bitify` about 1 month ago
AI Summary: Implement and formally verify the soundness and completeness proofs for the `Bits2Num` function within the `Bitify` module of the `clean` Lean DSL for zk-SNARK circuits. This involves writing Lean4 code to prove the correctness of the function's conversion of bit vectors to numbers.
Complexity:
4/5
good first issue gadget
[circomlib] Add remaining proofs in `Comparators` about 1 month ago
good first issue gadget
[circomlib] Prove `CompConstant` soundness and completeness about 1 month ago
good first issue gadget