As a fully open source effort, we of course want every aspect of the chip to be fully documented and auditable. It's useful to have something like a dedicated core to handle initial boot, but it's not useful to keep that core completely undocumented (e.g. the Intel Management Engine). Our answer there is what we term 'minion cores' (http://www.lowrisc.org/downloads/lowRISC-memo-2014-001.pdf), microcontroller-class cores to handle these sort of tasks. These are fully documented, open source, and implement the RISC-V ISA.
As for formal specifications, there has been some work on specifying the RISC-V ISA using L3 https://github.com/SRI-CSL/l3riscv. MIT have been working on a specifying using their 'Kami' tool as well.