I'm an Applied Scientist in the Automated Reasoning Group at Amazon Web Services, where I work on Dafny. In school I devoted a good chunk of my time to the Isabelle theorem prover. All that work is rather foundational, with some kernel dieting (📃, 📽️) and the formalization (📃, 📽️) of the metalogic Pure. Not so recently, I've dabbled in parallel numerics (📃, 📽️).

If you want to get in touch, your best bet is to email me.