Unsoundness is a concept understood in formal logic, which can have multiple manifestations in formal verification. Some of these are more direct, as in having a formally unsound logic, some are more abstract, e.g., having an unsound translation into executable target code. We will explore different notions that are captured by the concept of undsoundness and their (practical) implications for verification and theorem proving settings.