What assumptions does the later formal proof need beyond the toy color test, especially once you make it interactive or repeat it many times, do you still get zero knowledge under composition, or only for a single isolated run? Also, in the real systems you mention, what exactly is the leakage boundary, because a proof of a private balance or age claim can still leak a lot through timing, statement choice, or the fact that the verifier can adaptively query again.