TacTok: semantics-aware proof synthesis. - Emily First; Yuriy Brun; Arjun Guha (Proc. ACM Program. Lang., 2020)

Diversity-Driven Automated Formal Verification. - Emily First; Yuriy Brun (ICSE, 2022)

PRoofster: Automated Formal Verification. - Arpan Agrawal; Emily First; Zhanna Kaufman; Tom Reichel; Shizhuo Zhang; Timothy Zhou; Alex Sanchez-Stern; Talia Ringer; Yuriy Brun (ICSE Companion, 2023)

Baldur: Whole-Proof Generation and Repair with Large Language Models. - Emily First; Markus N. Rabe; Talia Ringer; Yuriy Brun (ESEC/SIGSOFT FSE, 2023)

Getting More out of Large Language Models for Proofs. - Shizhuo Dylan Zhang; Talia Ringer; Emily First (CoRR, 2023)

Passport: Improving Automated Formal Verification Using Identifiers. - Alex Sanchez-Stern; Emily First; Timothy Zhou; Zhanna Kaufman; Yuriy Brun; Talia Ringer (ACM Trans. Program. Lang. Syst., 2023)

Learn from Failure: Fine-tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving. - Chenyang An; Zhibo Chen 009; Qihao Ye; Emily First; Letian Peng; Jiayun Zhang; Zihan Wang 001; Sorin Lerner; Jingbo Shang (ACL (1), 2024)

CoqPyt: Proof Navigation in Python in the Era of LLMs. - Pedro Carrott; Nuno Saavedra; Kyle Thompson; Sorin Lerner; João F. Ferreira 001; Emily First (SIGSOFT FSE Companion, 2024)

Cobblestone: Iterative Automation for Formal Verification. - Saketh Ram Kasibatla; Arpan Agarwal; Yuriy Brun; Sorin Lerner; Talia Ringer; Emily First (CoRR, 2024)

Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification. - Kyle Thompson; Nuno Saavedra; Pedro Carrott; Kevin Fisher; Alex Sanchez-Stern; Yuriy Brun; João F. Ferreira 001; Sorin Lerner; Emily First (ICSE, 2025)

Lemmanaid: Neuro-Symbolic Lemma Conjecturing. - Yousef Alhessi; Sólrún Halla Einarsdóttir; George Granberry; Emily First; Moa Johansson; Sorin Lerner; Nicholas Smallbone (CoRR, 2025)