ProsaBuddy uses LLM agents to prove real-time schedulability lemmas, significantly outperforming existing Rocq proving agents and the general coding agent OpenCode on a mini benchmark
The work presents ProsaBuddy, an LLM-based agent system that uses a ReAct loop with retrieval over the Prosa codebase, access to Rocq tools and optional human-written hints, and a subgoal-delegation architecture that decomposes a lemma into subgoals dispatched to subagents for proof, and on a mini benchmark drawn from real-time scheduling literature it significantly outperforms state-of-the-art LLM-based Rocq automated proving agent systems and the general coding agent OpenCode.