Document the two lessons from taking a multi-document protocol suite through clean-room proof: use an independent multi-reviewer panel (the verdict is a sample, not a theorem), and add a joint cross-document proof (per-document proofs can pass in isolation while the seam between them stays broken). Tie both into the clean-room invariant and the success criteria. leaf check-in: 64deb0b261 user: dmestas tags: trunk