New formally verified proof of #safegcd iteration bound: https://cr.yp.to/2023/hull-light-20230416.sage (script for full run+extras: https://cr.yp.to/2023/hull-light-howto-20230416.sh) Advantages over previous formally verified proofs: (1) covers all input sizes; (2) finishes verifying in 10 minutes; (3) smaller TCB (HOL Light).