A proof could be valid, and the same deposit could still be withdrawn twice. That was the problem at the center of Tornado Crash, the challenge I wrote for BlazCTF 2023.
A capture-the-flag competition, or CTF, gives players deliberately vulnerable programs and asks them to find a way through. My challenge involved a withdrawal protected by a zero-knowledge proof: a way to demonstrate that a withdrawal is authorized without revealing the secret used to authorize it.
The contract, a program running on the blockchain, kept a record of used nullifiers, the values that stop a withdrawal from being claimed again. Present a nullifier it has already seen and the withdrawal is rejected. It sounds like a straightforward guest list: one name, one entry.
But the proof system and the contract did not agree on what counted as the same name.
The proof worked with numbers modulo a large prime, p. In that arithmetic, adding p brings you back to the same value. The contract stored ordinary integers. It could see x and x + p as different entries even though the proof treated them as equivalent.
A smaller example makes the mismatch easier to see. Modulo seven, 3 and 10 mean the same thing. In an ordinary list of integers, they are different. If one part of a system checks the arithmetic while another records the integer, submitting both can look like two different requests.
The missing range check left room for both representations. The challenge used Miximus, a cryptocurrency mixer designed to let people deposit and withdraw without publicly linking the two. The vulnerability sat at the boundary between verification and the contract’s record of withdrawals. There was no need to break the underlying cryptography to exploit that disagreement.
That boundary is an interesting place to begin reading a zero-knowledge application. Pick one input and follow it. Check how it is represented when it enters the contract, how the proof interprets it, and what gets written afterward. A large proof system can sit next to a very small mistake.
This distinction connects to our work on Coda (Liu et al., 2023). Coda uses refinement types, types enriched with logical properties, to state and check what a circuit should mean. The research question is whether the encoded constraints imply the intended property. In Tornado Crash, the property also crosses the boundary into the contract that records withdrawals.
For this challenge, the decisive question is whether every accepted nullifier has one permitted representation. Until the answer is yes, “we have seen this withdrawal before” depends on which side of the interface you ask.