Following line generate a sha512 secret via jdk's KeyGenerator.
SecretKey secretKey = KeyGenerator.getInstance("HmacSHA512").generateKey();
I am wondering is the key random secure?
Or, should I init the generator with a SecureRandom instance explicitly, before generate the key?
Just for completeness you could call the init method using a key size of 512 bits. However, the default key size of HMAC is the same size as the output. So in that sense it is very reasonable to assume that this key size is set by default. Indeed, calling the init method using a constant value should be avoided.
As for the implementation, it is as likely that if you don't call the init method explicitly that a default value is assumed and that a SecureRandom instance is chosen. However, you are correct in the sense that this is a logical provider default; it should have been specified as a requirement to all providers.
Some idea from what is going on here is in KeyGeneratorCore. All of the provider code is online, so not finding it is up to not looking deeply enough, although admittedly you need some Google foo to find it.