I have only basic knowledge of this but it feels like it should be possible to mathematically prove the correctness of bignum implementation, even if it's in C,

I have only basic knowledge of this but it feels like it should be possible to mathematically prove the correctness of bignum implementation, even if it's in C, no? And it would be very valuable work too.