About

Hi! I’m Tanner. I am a formal verification software engineer at Nexus, building and verifying the Zero-Knowledge Virtual Machine. I graduated from the University of Pennsylvania with an MSE in computer science and a BA in mathematical logic. My academic interests include formal verification, programming languages, category theory, type theory, and all things logic.

I am an avid user of the Lean theorem prover and I have done contracting work formalizing mathematical proofs for Harmonic and Project Numina. Independently I have made contributions to Mathlib and enjoy formalizing things related to logic and programming languages.

I have participated in the Adjoint School, doing research in categorical semantics of compositional reinforcement learning, under supervision of Georgios Bakirtzis and Michail Savvas. Previously I have interned with Amazon’s Automated Reasoning Group, and at Meta.

Outside of work I enjoy reading philosophy, in particular analytic philosophy, philosophy of mind and consciousness, metaphysics, and Eastern philosophy and mysticism. I played 2 years of D1 football at Penn and I enjoy lifting weights, yoga, and running. I am also learning guitar (primarily 90s grunge) and am passionate about veganism and total liberation for all beings.

Nexus team at Summit V, June 2025