RISC-V is an open specification that can be implemented by proprietary and open source efforts alike. This means there's nothing stopping someone else doing a RISC-V SoC that, like most current commercial cores, has documentation "protected" by an NDA and inaccessible to most users.
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.
Take a look at http://fossi-foundation.org/. Whatever terminology you're using, I think it's right to say lowRISC and FOSSi have a shared vision for free and open source designs that respect user freedom.
Open source as defined by the OSI describes something identical to free software as described by the FSF.
* "Free software" and "open source software" are two terms for the same thing: software released under licenses that guarantee a certain, specific set of freedoms.
Sure, I just meant that RISC-V being permissively licensed with in-depth documentation available will ease formally verifying implementations of it, and also encourage open-source implementations.
On the minion cores: that sounds quite interesting and I'm reading the paper now. Are they very different from e.g. the USB and network chips on the RPi, aside from having open firmware?
For the initial iteration of minion cores, think of them as being an openly documented boot core and a way of implementing low-speed I/O in software (with some extra hardware support for things that would be dumb to do in software, e.g. shifting out a register). The initial target is SPI, I2C, I2S etc. Over the longer term, we are interested in using modified RISC-V cores for high-speed I/O and in general increasing the flexibility of a typical SoC design.
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.