ExtendedStaticChecking for JavaLanguage
See
http://secure.ucd.ie/products/opensource/ESCJava2/
http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/docs/ESCJAVA-UsersManual.html
For an idea how this works see ProofAnnotationsForBubbleSort.
There seem to be versions for Modula 3 and Haskell now:
For a general review see http://radu.ucd.ie/hp/papers/phd.pdf