Comment by js8

If you're able to detect where you use these hard-to-analyse functions, then yes. This is feasible on source level, and maybe known compiler binary level. I think ultimately people will want to validate properties of binary code against the model specification of their hardware.

Although the prover might be smart enough to say, "this function is getting kinda complicated, let me model it as a random variable and see if it's enough". I think LLMs can kinda do it but not sure if your typical theorem provers can (it's on the level of being able to employ probabilistic proof techniques).