>they are the basic component of hardware (and software) formal verification systems.

They are _a_ component. It's quite possible to perform formal verification without them, for instance the CompCert verified C compiler, or the DeepSpec end-to-end verification project: https://deepspec.org/main. SAT solvers generally have poor support for constructive logic, the kind of logic used in theorem provers based on dependent types like Coq. Systems based on classical logic like HOL integrate better with SAT solvers, but the lack of dependent types makes a lot of things much cumbersome to prove, especially if one wants proofs that can be extracted to programs.