I have contributed nearly 10K lines of machine checkable, formalized programs and proofs and made 56 commits as part of a large-scale, open source formal verification project. I have formalized parts of my honors thesis, helped to refactor code, and formalized important higher coherences arising in Homotopy Type Theory.