> But now, I could grab picorv32 or rocket for free off the internet. Both have been taped out in this capacity before, both speak standard bus interfaces, and the former has been fully formally verified.

What do you mean by "fully formally verified"? My understanding is that picorv32 has been verified by riscv-formal, and riscv-formal performs bounded model checking, which is not full formal verification unless you otherwise establish an upper bound on trace lengths that must be considered to find a bug.