alt Hacker NewsContracts 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)
You sounds like you have more experience than me in this space (specifically contracts). I'm curious if you have any examples right off hand that would need whole program analysis. I need more examples to throw at my toy language that's not just another lock free work stealing queue.