[samatman]

It is an interesting problem to think about, for sure.

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.

[adpcm]

There is indeed research and literature about this. For example “Formal verification of multiplier circuits using computer algebra”, Daniela Kaufmann, see https://danielakaufmann.at/publications/

These kinds of methods are used in EDA Formal Verification tools to check real multipliers, FMAs, dot-products etc in CPU & GPU designs.