I'm not so sure that's true. You can rent a Skylake chip on Google Cloud that'll perform 1.6 trillion 64 bit operations per second for $0.96/hr preemptively. That's enough to run one instruction over a 64 bit address space exhaustively over 120 days, or for ~$2800.

Obviously that needs to be multiplied by the number of instructions a test needs to execute (and it has to be well written with AVX 512), but we're not talking nation state levels of resources here for simple cases, and that figure is only going to drop further with time.

Not to mention the potential for FPGA or ASIC implementations if the tests are important enough.

Hmm that's surprisingly within reach. I bet you could crowd-source that kind of verification with BOINC.

Check out DeepState! https://github.com/trailofbits/deepstate

It's hard to give a general strategy without knowing the problem structure, but I guess you could say one general strategy is to exploit the problem structure in a way that lets you test multiple values in one shot.

Feed llvm bytecode through Z3 and hope you didn't implement something with cryptographic behaviour.

Could you give some advice or pointers on this?

This should get you going. Come back if you get stuck. https://twitter.com/whitequark/status/915211914443153409

Edit: sorry, I just don't have the time to get you the details.