[bluGill]

The other hope for contracts is static whole program analysis can prove your program - at least in part. If you can prove some contract false that tells you where a bug is long before anyone triggers it.