I am a researcher and educator specializing in formal verification, interactive
theorem proving, and verified compilers. I build practical tools, grounded in
foundational theory, that ensure end-to-end correctness of complex software
systems. My recent work explores AI-assisted proof mechanization: leveraging
LLMs to dramatically accelerate the development of machine-checked proofs for
verified software.
I obtained my PhD from Princeton University, advised by
Andrew Appel,
where I worked on certified compilation of functional languages.
Students
Current
Lefteris Lazaropoulos, Master's Student
From EVM bytecode to mechanized reasoning in proof assistants
Petros Aggelatos, Master's Student
Verified differential data flow in Lean
Georgios Alexandros Georgantzas, Master's Student
A verified library for reasoning about algorithmic stability in Lean, co-advised with Kyriakos Fountoulakis
Past
Anvay Grover, Senior Thesis, Fall 2019 / Spring 2020
Implementation and Verification of the CPS Transformation of the CertiCoq Compiler, co-advised with Prof. Andrew Appel
Katja Vassilev, Senior Thesis, Fall 2018 / Spring 2019
Implementation and Verification of the Dead Parameter Elimination Optimization of the CertiCoq Compiler, co-advised with Prof. Andrew Appel
Academic Service
Co-chair, RocqShop 2026
Program Committee, PLDI 2026
Program Committee, PLDI 2023
Program Committee, Types 2022
Workshops Co-chair, ICFP 2022
Program Committee, PEPM 2022
Program Committee, CPP 2022
Workshops Co-chair, ICFP 2021
Program Committee, PriSC 2021
Program Committee, TFP 2020
Program Committee, ML 2019
External Review Committee, ICFP 2019
Program Committee, TyDe 2018
Program Committee, OCaml 2017
Artifact Evaluation Committee, POPL 2017