I am curious about the strongest methods we know of that can allow us to discover (arithmetical) unsoundness or nonstandardness in a foundational system $S$ that interprets at least ACA (such as ZFC). Detecting (arithmetical) inconsistency is 'easy'; $S$ is inconsistent iff $S$ proves (the transl...