Software contracts, or specifications, define the intended behavior of systems. They are used by the Dafny programming language to check that an implementation of a system is a safe substitution for the contract that defines it. Writing contracts is error-prone and there are limited tools for detecting their faults. We present a solution that detects four common pitfalls in Dafny contracts. The pitfalls are contradictions, vacuity, unconstrained outputs, and redundancy. The ideas and algorithms presented can be extended to other contract-based languages.