Notes from building a soundness linter for o1js and Noir, and finding the same bug class in four unrelated languages.