For my Advanced Topics in Principles of Programming Languages Class, I wrote a compiler for a fragment of ML based on a talk given by Max New. A full report, including detailed descriptions of the intermediate representations, proofs of correctness, as well as an implementation, can be found on my Github
Used group theory and SAT solvers to find and verify the most adversarial board in the Keep Talking and Nobody Explodes module Hexamaze. A blog post detailing this project can be found here.