Large language models (LLMs) and proof assistants are in the early days of a fruitful marriage. LLM-based agents draft and mechanize, while proof assistants provide infrastructure to construct proofs and check the results. We consider two aspects of safety when integrating agents with the Isabelle proof assistant. First, we survey technological methods for isolating agents and restricting what they can do through Isabelle. Second, we discuss different agentic workflows and the human intervention needed to assure the resulting artifacts' logical consistency.
Paper draft