2023.04.16 21:11:27 (Mastodon 110210546878026581, Twitter 1647709221662646274) from Daniel J. Bernstein:
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).