Comment by bluGill

Contracts are written such that the compiler can diagnose a detected violation if it wants to. However most contracts realistically need whole program analysis to diagnose and no compiler can do that - you want a separate static analysis for that. (this doesn't exist, but there is hope people start writing those)