Tanner Duve

Proof Engineer, Logician

pfp1.png

Hi! I’m Tanner. I am a Member of Technical Staff at Logical Intelligence, working on formal verification and compilers. 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.

Previously I worked on programming languages and formal verification with Amazon’s Automated Reasoning Group, and I have done research in applied category theory with Georgios Bakirtzis and Michail Savvas.

My primary working language is Lean, for both formalization work and verified software development. I have contributed to Mathlib and CSLib, and I am an author of Algolean, a Lean library for formalizing algorithms and their complexity.

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, and am passionate about veganism and total liberation for all beings.