In the traditional world of raw Verilog, gate-level tuning, verification systems with millions of lines of code and all that, that's true. By the way, those hundreds of people will need a bunch of million dollar tools, hardware and software. And a lawyers dealing with the license and patents, if you are going to sell your chips - and of course you are going to sell your chips in traditional hardware world, except you are DoD or NASA.

But maybe the hardware world is not have to be this way and this way only.

> No part of Kami need be trusted beside the formalization of low-level (Verilog-style) circuit descriptions; all other aspects have end-to-end correctness proofs checked by Coq. Hardware designs are broken into separately verified modules, reasoned about with a novel take on labeled transition systems. Furthermore, Coq provides a natural and expressive platform for metaprogramming, or building verified circuit generators, as for a memory caching system autogenerated for a particular shape of cache hierarchy, or a CPU generated given a number of concurrent cores as input.

> We have been developing a candidate official formal specification for RISC-V, which stands a good shot at being ratified soon as such by the RISC-V Foundation. The spec now includes virtual memory and is able to pass all the official RISC-V machine-code tests that aren't marked as specific to particular extensions. We should be able to boot Linux on the specification soon, running as a simulator.

> A verified processor exists providing all that functionality, though we are still working on debugging the specification, since the current version isn't quite able to boot an operating system (so the specification must be out-of-synch with software expectations somehow).

https://deepspec.org/entry/Project/Kami