Where is HChaCha20 formally defined?
Doing further research accross multiple scientific portals and cryptography-related forums, it turns out that no formal specification exists… at all.

HChaCha20 can be constructed exactly the same way as HSalsa20, but has not really been specified or analysed to the full extend we usually expect cryptographic designs to be specified and analysed.

In this relation, it seems to make sense to also quote what CodesInChaos commented:


  I don't think such a spec exists. For the security, you can just directly transfer the "if Salsa20 is secure so is HSalsa20" proof to "if ChaCha is secure, so is HChaCha". Related: Can I use the ChaCha core as a 256-bit to 256-bit one-way function?


The same conclusion can be drawn from postings to the Cfrg mailing list (example):


  …
  The proof for XSalsa20/HSalsa20 should work for XChaCha20/HChaCha20 too
  afaics. (http://cr.yp.to/snuffle/xsalsa-20110204.pdf
  on http://cr.yp.to/snuffle.html)
  …