本文对 Go 标准库 `crypto/internal/fips140/bigmod` 中的 `extendedGCD` 实现进行了形式化验证。该实现用于 RSA 密钥对生成中的扩展欧几里得算法，是从 BoringSSL 移植而来。然而，研究者发现了两处偏差：一是系数更新方式与原始实现不同，二是允许更大的输入域。第一个偏差导致算法不变量被破坏，第二个偏差使得原有证明不再适用。研究者修复了第一个偏差（性能提升平均 24%），并针对第二个偏差将 BoringSSL 的证明移植并扩展到更大的输入域。他们使用 Go 语言专用验证器 Gobra 证明了修复后实现的正确性和终止性，并借助 Lean 验证了一些非线性算术引理。验证过程表明，即使是经过充分审查的代码也可能存在细微错误，形式化验证是发现此类错误的有效工具，而 AI 代理可通过迭代优化不变量和引理来辅助验证。