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.