I'm a bit confused - they recently discovered Java is unsound? I thought this was well-known for quite some time because of broken co/contravariance?

On recent Java developments, Java's undecidable typechecking has now been proven:

http://dl.acm.org/citation.cfm?id=3009871