[throwaway40483]

Not only is formal methods more effective for HW, the incentives are also more tilted towards HW. If you fuck up the HW design, well..you're fucked. With SW, "you can always push out an update" mentality exists. I'm not saying this to criticize SW, but this is more an example of how you conform to the ecosystem in which you exist.

[DennisP]

Which is why people are keen on developing formal methods for smart contracts, which generally can't be updated. Plus they're a lot smaller than most software.