Just noticed this:
http://google-opensource.blogspot.com/2011/02/contracts-for-java.html
It sounds like they're oblivious to the higher-order issues (the pictorial demo, for example, makes it sound like contract checks only involve immediately-verifiable -- i.e., first-order -- properties).
Too bad these guys didn't know to ask Jacob for help! :)
Dave