I used to work for a chip company. For the first 10 or so years I was there formal methods were 'some time in the future' However a year or so before I left (in

I used to work for a chip company. For the first 10 or so years I was there formal methods were 'some time in the future' However a year or so before I left (in 2013) a formal tool called Jasper popped up that was really productive in silicon verification (that is, testing/QA, but taken really seriously). It didn't cover everything - sometimes it got stuck and you had to test that case the old way. But it did a lot of work. The tool could do formal proofs, although when I left it wasn't used in the way theorem-prover people seem to imagine them being used: starting by a full model of what the workpiece should do. Instead, it was used to prove assertions were always/never true. But in HW we have a lot of assertions :-) For software there are a couple of issues: one is that the state is a lot bigger (in theory of course HW state is a superset of SW state, but in practice the content of most RAM can be regarded as just content and you don't need to prove anything about it other than that it is copied okay). The other is that with the skimpy amount of testing most teams do, there isn't a huge pressure to find a way to reduce testing costs like there is in HW (where 2 engineers writing tests to one writing verilog isn't unusual).