There are tools for formal verification of design input, and they are being used, but not for everything.
Why there are still errata for silicon
1. Writing a formal specification of your intended behavior is hard and the best verification tool doesn't help when your assertions don't encode the required or intended behavior. So even with 100% formal coverage, you would still get erratas. And some people don't write any formal verification, instead working with a simulation based approach (either hand-written test cases or random stimulus simulation)
2. Computation complexity of formal verification is exponential. At some point you simply can't formally prove the behavior of a design, because it just won't run on your server.
3. There's different levels of formal verification, not all of them are in the spec -> behavior path. For example, you could classify automated checks like logic equivalence between the synthesis netlist and RTL code as a formal verification. But that checks if the optimizer in the synthesis tool was correct, not that you wrote the correct RTL.
Would be really nice honestly. But I don't think it will be coming anytime soon, it's just too expensive to build a chip.
The one-time costs for masks are just much more expensive as for PCBs, so wafer shuttle services are still really expensive when pooled PCBs are really cheap.
And any machines that would be cheaper for prototyping (direct laser writing or direct e-beam writing) don't scale to mass production.
You can already make (tiny) chips for a somewhat affordable cost with tiny tapeout.
But that's still not nearly as cheap as PCB prototypes and with much longer wait times.
Why there are still errata for silicon
1. Writing a formal specification of your intended behavior is hard and the best verification tool doesn't help when your assertions don't encode the required or intended behavior. So even with 100% formal coverage, you would still get erratas. And some people don't write any formal verification, instead working with a simulation based approach (either hand-written test cases or random stimulus simulation) 2. Computation complexity of formal verification is exponential. At some point you simply can't formally prove the behavior of a design, because it just won't run on your server. 3. There's different levels of formal verification, not all of them are in the spec -> behavior path. For example, you could classify automated checks like logic equivalence between the synthesis netlist and RTL code as a formal verification. But that checks if the optimizer in the synthesis tool was correct, not that you wrote the correct RTL.