zksecurity launched a lean4 challenge to formally verify zk circuits as cheaply as possible, but a loophole in the verification let the leaderboard at QED audit be taken over

1 min

zksecurity opened a challenge to formally verify zk circuits in lean4 as cheaply as possible, but there was a loophole in the verification method, so QED audit ended up taking over the leaderboard.

In the challenge, when verifying soundness and completeness, they follow a p -> q proposition; since if p is false the implication is always true, it looks like they set p to be false across the board and passed (not sure if that’s exactly right).

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