Wei Dai on the Orchard zk circuit bug and the case for formal verification

A thread by researcher Wei Dai examining the Orchard zk circuit bug as reported by Taylor Hornby. Dai walks through the under-constrained circuit step, observes that the error "looks obvious in retrospect" yet was missed by highly capable protocol designers, cryptographers, and auditors, and warns the situation "may get worse before it gets better." The thread is used here for its argument that hand-audited zero-knowledge circuits are prone to exactly this class of latent soundness error, and that formal verification offers a stronger guarantee than human review alone.

It contributes the expert-reaction and methodology angle: not just what broke, but why this category of bug is hard to catch and what might reduce its recurrence.