I'm a member of technical staff at Axiom Math working on AI-driven software verification at scale. My work applies concepts from programming languages theory to problems in formal verification and mechanized proof, including compilers, automated reasoning, and systems verification. Given the recent intersection of formal methods and AI and the rapid scaling of proofs, I believe efforts to improve our systems of formal reasoning are more critical than ever.

Previously, I completed my PhD at MIT advised by Adam Chlipala. During my PhD, I developed a mechanized framework for extension-proof compiler verification based on modular specifications for programming languages and built verified automation for language-agnostic reasoning. I completed my Bachelor's degree at Northeastern University, where I researched gradual typing, parametric polymorphism, and compositional compiler correctness in Amal Ahmed's group. See my CV here.

Papers and Workshop Talks

Verified E-Graphs for Automating Compiler Verification.
Dustin Jamner, Tilek Askerbekov, and Adam Chlipala.
To appear in the 54th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '27). Mexico City, Mexico. January 2027.

Efficient Proof Engines with Lambda-DAGs.
Jon Rosario, Dustin Jamner, Adam Chlipala, and Andres Erbsen.
To appear in the 54th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '27). Mexico City, Mexico. January 2027.

Pyrosome: Verified Compilation for Modular Metatheory.
Dustin Jamner, Gabriel Kammer, Ritam Nag, and Adam Chlipala.
In the International Conference on Object-Oriented Programming, Systems, Languages & Applications (OOPSLA '25). Singapore. October 2025.

Foundational Integration Verification of a Cryptographic Server.
Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel, and Adam Chlipala.
In the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '24). Copenhagen, Denmark. June 2024.

Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilation.
Dustin Jamner, Gabriel Kammer, and Adam Chlipala.
In the Ninth International Workshop on Coq for PL (CoqPL 2023). Boston, Massachusetts, USA. January 2023. Workshop talk.

Relational Compilation for Performance-Critical Applications.
Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, and Adam Chlipala.
In the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '22), San Diego, California, USA. June 2022.

Graduality and Parametricity: Together Again for the First Time.
Max New, Dustin Jamner, and Amal Ahmed.
In the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '20), New Orleans, Louisiana, USA. January 2020.

Using Binary Analysis Frameworks: The Case for BAP and angr.
Chris Casinghino, Michael Dixon, Jt Paasch, Cody Roux, John Altidor, and Dustin Jamner.
In the NASA Formal Methods Symposium (NFM '19), Houston, Texas, USA. May 2019.

Theorems for Free for Free: Parametricity, With and Without Types.
Amal Ahmed, Dustin Jamner, Jeremy Siek, and Philip Wadler.
In the ACM SIGPLAN International Conference on Functional Programming (ICFP '17), Oxford, UK. September 2017.
Technical report, June 2017.