zksecurity에서 lean4로 최대한 저렴하게 zk회로를 정형 검증하는 챌린지를 열었는데.. 검증 방식에 허점이 있어서 QED audit에서 리더보드 점거해버렸네요.

챌린지에서 soundness랑 completeness를 검증할 때 p -> q 식의 명제를 따르는데, p가 거짓이면 항상 결론이 참이 되니 죄다 거짓인 p를 설정해서 통과해버린듯 (정확한지는 모름)

설명: https://x.com/QED_Audit/status/2075400032937775326?s=20