How Hard Can It Be to Formalize a Proof? Lessons from Formalizing CryptoBox Three Times in EasyCrypt. - François Dupressoir; Andreas Hülsing; Cameron Low; Matthias Meijers; Charlotte Mylog; Sabine Oechsner (IACR Cryptol. ePrint Arch., 2025)