I am looking for motivated students interested in formal verification, interactive theorem proving, verified compilers, and AI-assisted proof mechanization. Below are some available thesis topics. If you are interested, please get in touch.
LLM-Assisted End-to-End Verification of the CertiRocq Compiler
Use LLMs to fill verification gaps in the CertiRocq compiler pipeline and work toward an end-to-end correctness theorem.
Requires familiarity with Rocq (Coq) and functional programming.
Verified Library Implementations in Lean
Develop verified implementations of data structures and algorithms in the Lean proof assistant, with extraction to mainstream languages via foreign function interfaces.
Requires familiarity with functional programming and interest in theorem proving.
AI-Assisted Proof Mechanization
Explore and evaluate the use of LLMs for mechanizing mathematical proofs in interactive theorem provers (Rocq, Lean).
Requires interest in formal verification and AI.