Induction proofs work fine. And 3SAT can check that your logic is equivalent.
The bigger issue is that multipliers are subject to runtime errors just like memory--so how do you check for that? The answer is that you build a multiplier that works on a smaller field (modulus) and then you check that against the big multiplier's result. If they differ, you flag.
I seem to recall that only Hitachi and IBM had processors that did this.
My suspicion is that this kind of verification is amenable to breaking down into stages, essentially by drawing boxes around highly-connected regions, proving those properties exhaustively, then treating the various interconnects as between two black boxes with those known properties.
I'm sure there's some deep literature on this subject, I don't even know where to begin looking for it however.
