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 as a software engineer writing Rust at Nexus. I have done research in applied category theory with Georgios Bakirtzis and Michail Savvas, and in programming languages and formal verification with Amazon’s Automated Reasoning Group.

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