Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Joshua M. Cohen; Stephanie Weirich (J. Funct. Program., 2021)

Verified Erasure Correction in Coq with MathComp and VST. - Joshua M. Cohen; Qinshi Wang; Andrew W. Appel (CAV (2), 2022)

Specifying and Verifying a Real-World Packet Error-Correction System. - Joshua M. Cohen; Andrew W. Appel (VSTTE, 2023)

A Formalization of Core Why3 in Coq. - Joshua M. Cohen; Philip Johnson-Freyd (Proc. ACM Program. Lang., 2024)

Formally Verified Cloud-Scale Authorization. - Aleks Chakarov; Jaco Geldenhuys; Matthew Heck; Michael Hicks 001; Sam Huang; Georges-Axel Jaloyan; Anjali Joshi; K. Rustan M. Leino; Mikael Mayer; Sean McLaughlin; Akhilesh Mritunjai; Clément Pit-Claudel; et al. (ICSE, 2025)