Still, this is not a bad situation overall. If you are forced to trust the C compiler to correctly compile C, and the hardware to correctly implement the instructions in the documentation, well, you're already forced to trust both of those every day.

So this doesn't give you an absolute proof of correctness. But it does substantially reduce the size of the problem, which is now limited to (1) verifying that you actually proved what you think you did, and (2) all the stuff you were normally trusting anyway. (Some of the stuff you were trust anyway is broken, of course.) But this is a smaller problem than trusting 1,000 lines of highly-optimized CSG code written by a model we don't actually understand.