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

ProsaBuddy is an LLM-based agent system aimed at mechanized real-time schedulability proofs, intended to lower the effort needed to develop machine-checkable proofs in the Rocq proof assistant on top of Prosa. Prosa already offers a foundation for machine-checkable schedulability analysis proofs, but the substantial time and expertise required to construct such proofs remain a barrier to wider adoption; this work brings LLM agents into that proof-construction step. Evidence comes from the abstract-level system description and evaluation statement; no counts of proved lemmas, success rates, or benchmark size are given.

The system employs a ReAct loop combined with retrieval over the Prosa codebase, access to Rocq tools, and optional human-written hints. Retrieval, tool access, and optional human hints are integrated into a single agent loop rather than relying only on the model to generate proof scripts. The abstract explicitly lists these three mechanisms but gives no retrieval granularity, tool-interface detail, or hint-injection scheme.

The system uses a subgoal-delegation architecture that decomposes a lemma into subgoals and dispatches them to subagents for proof. Proof search is organized by decomposition and delegation, in contrast to a single agent proving end to end. The abstract provides the architectural description but reports no ablation on the decomposition strategy or the effect of subgoal granularity.

On a mini benchmark drawn from real-time scheduling literature, ProsaBuddy significantly outperforms state-of-the-art LLM-based Rocq automated proving agent systems and the general coding agent OpenCode. The comparison covers both a specialized Rocq proving agent and a general coding agent, positioning the system relative to two kinds of baselines. The abstract states only that performance is significantly better; it gives no benchmark item count, pass rate, or statistical test detail.

The result targets the setting of building machine-checkable real-time schedulability proofs in the Rocq proof assistant on top of Prosa, and is meant for real-time systems and formal methods researchers who want to reduce proof-construction effort. The design supports optional human-written hints, indicating a role as assistance rather than full replacement of human proof work. Evaluation is scoped to a mini benchmark drawn from real-time scheduling literature, so the conclusions apply to the lemma types and proof tasks that benchmark covers.

The reading scope here is the abstract only, without body text, figures, or experimental detail, so the benchmark's item count, success-rate numbers, per-baseline comparisons, and statistical significance cannot be confirmed here. How the subgoal-delegation architecture behaves across different lemma structures, how much retrieval and human hints each contribute, and how the system behaves on larger proof tasks remain open questions worth watching.