  Proof assistants enable users to develop machine-checked proofs regarding
software-related properties. Unfortunately, the interactive nature of these
proof assistants imposes most of the proof burden on the user, making formal
verification a complex, and time-consuming endeavor. Recent automation
techniques based on neural methods address this issue, but require good
programmatic support for collecting data and interacting with proof assistants.
This paper presents CoqPyt, a Python tool for interacting with the Coq proof
assistant. CoqPyt improves on other Coq-related tools by providing novel
features, such as the extraction of rich premise data. We expect our work to
aid development of tools and techniques, especially LLM-based, designed for
proof synthesis and repair. A video describing and demonstrating CoqPyt is
available at: https://youtu.be/fk74o0rePM8.
