GCD: Garbled, Corrected, Demonstrandum -- Fixing and Proving Go's Extended GCD Implementation
Researchers verified and fixed subtle bugs in Go's standard library extended GCD implementation to ensure correctness for RSA key generation. They found deviations from a reference implementation regarding coefficient updates and input domain handling, which broke mathematical invariants. Using formal verification tools like Gobra, they proposed fixes that improved performance by about 24% on average.