Given some model of the way circuits work, it's possible to formally verify hardware as well. Maybe your model doesn't quite match reality and your system will

Given some model of the way circuits work, it's possible to formally verify hardware as well. Maybe your model doesn't quite match reality and your system will still fail. But redundant systems can also experience simultaneous failures of their components. It would be interesting to know which approach is more effective.