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&#x27;s in C, no? And it would be very valuable work too.