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)

Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness. - Pedro Carrott; Sacha-Élie Ayoun; Azalea Raad (ECOOP, 2025)

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)

Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness (Artifact). - Pedro Carrott; Sacha-Élie Ayoun; Azalea Raad (Dagstuhl Artifacts Ser., 2025)