2023.07.26 13:46:28 (Mastodon 110780690497105946, Twitter 1684198514543165441) from Daniel J. Bernstein:
Formally verified theorems about decoding Goppa codes: https://cr.yp.to/2023/leangoppa-20230726-verify.html This is using the Lean theorem prover; I'll try formalizing the same theorems in HOL Light for comparison. This is a step towards full verification of fast software for the McEliece cryptosystem.