PaperlayerView exact revision on arXiv

Source-linked AI summary

ProsaBuddy: Assisting Mechanized Real-Time Schedulability Analysis with LLM-based Agents

Junyi Liu, Tianchi Ren, Fei Guan, Xu Jiang, Zhe Jiang, Wang Yi, Nan Guan

arXiv:2610.03796v1cs.LOcs.AI

TL;DR

Mechanized schedulability proofs are time-consuming, and the limited Prosa corpus constrains LLMs’ ability to learn domain-specific proof patterns. ProsaBuddy combines agent-based proof construction with Prosa retrieval, Rocq feedback, and optional human hints; evaluations report superiority on a larger Prosa-lemma set and success on many non-trivial lemmas.

  • Problem

    Developing Prosa proofs can take weeks, while the limited Prosa corpus constrains LLMs’ ability to learn schedulability-specific proof patterns.

    Source: §I · p. 1, A. Overview · p. 3

  • Method

    ProsaBuddy uses LLM agents with Prosa retrieval, Rocq-tool feedback, optional human hints, and subgoal delegation.

    Source: §I · p. 1, A. Overview · p. 4

  • Results

    Evaluations on a larger set of Prosa-library lemmas confirm ProsaBuddy’s superiority, and it proves many non-trivial lemmas.

    Source: §I · p. 2, §V · p. 12

  • Takeaways & Limitations

    ProsaBuddy can assist with lengthy Rocq proofs, while the authors describe the work as preliminary with room for further exploration.

    Source: §V · p. 12

    The proving skills and guidelines are tailored to current LLM capabilities and may become obsolete as models improve.

    Source: §V · p. 12

Abstract

from arXiv · show

Rigorous schedulability analysis is essential for the design of hard real-time systems, yet errors in pen-and-paper proofs threaten the safety of critical applications. The Prosa initiative addresses this by offering a foundation for building machine-checkable schedulability analysis proofs in the Rocq proof assistant. However, the substantial time and expertise required to construct such proofs remain a major barrier for wider adoption of Prosa. This work presents ProsaBuddy, an LLM?based agent system designed to lower the effort needed to develop mechanized real-time schedulability proofs. ProsaBuddy employs a ReAct loop with retrieval over the Prosa codebase, access to Rocq tools and optional human-written hints. It uses a subgoal?delegation architecture, decomposing a lemma into subgoals and dispatches them to subagents for proof. We evaluate ProsaBuddy on a mini benchmark drawn from real-time scheduling literature. Experiment results show that ProsaBuddy significantly outper?forms state-of-the-art LLM-based Rocq automated proving agent systems and a general coding agent OpenCode

I. INTRODUCTION

Prosa offers machine-checkable schedulability proofs, but constructing them in Rocq can take weeks and hinder adoption. ProsaBuddy combines LLM agents and Prosa resources; evaluations report superiority over competing systems and success on non-trivial lemmas, while retaining a human-assistance role.

I. INTRODUCTION

  • Prosa provides definitions and proofs for machine-checkable schedulability analysis, addressing errors reported in pen-and-paper analyses of safety-critical systems –.The paper notes that such errors can have disastrous consequences.Source: §I · p. 1
  • Developing Rocq proofs in Prosa can take several weeks, creating a practical barrier to broader adoption.The authors report this estimate even for researchers with moderate familiarity with Prosa and Rocq.Source: §I · p. 1
  • ProsaBuddy combines a ReAct loop, retrieval over Prosa, Rocq-tool feedback, optional human hints, and delegation of subgoals to agents.The primary agent decomposes a lemma and dispatches subgoals to subagents.Source: §I · p. 1
  • ProsaBuddy significantly outperforms competing systems on a 24-lemma benchmark and shows superiority on a larger set of Prosa-library lemmas.The benchmark lemmas come from real-time scheduling literature and are absent from the existing Prosa library.Source: §I · pp. 1–2
  • ProsaBuddy proves non-trivial lemmas, including some requiring hundreds of Rocq tactics, but is not positioned as a replacement for researchers or a fully independent prover.It is intended to reduce tedious low-level proof work so researchers can focus on high-level proof ideas.Source: §I · p. 2

II. BACKGROUND AND RELATED WORK

The background introduces Rocq’s explicit proof workflow and Prosa’s verified scheduling foundation. It then surveys automation and identifies a gap in reusable, domain-specific proof procedures for real-time scheduling.

A. Rocq

  • Rocq proofs require explicit tactics to transform proof states, so even an intuitive schedulability claim can require many detailed steps.The paper describes Rocq as an interactive proof assistant based on dependent type theory.Source: A. Rocq · p. 2, Figure 1 · p. 2

B. Prosa

  • Prosa is a Rocq-based foundation for verified scheduling theory, emphasizing readable specifications, explicit assumptions, and proof reuse.Its boolean-predicate specifications support reflection-based proof automation, and the library focuses on a core subset of scheduling theory.Source: B. Prosa · p. 2

C. Automated Theorem Proving

  • Earlier Rocq automation includes proof-pattern reuse, external-solver integration, tactic frameworks, and learned tactic prediction, –.These approaches reduce routine effort but do not eliminate expert work decomposing goals and coordinating proof strategies.Source: C. Automated Theorem Proving · pp. 2–3
  • LLM-based provers increasingly combine synthesis, retrieval, feedback, repair, and agentic control –,,, [42], but do not expose domain-specific proof procedures as reusable skills.The paper identifies this as a gap between general proof generation and domain-aware automation for real-time scheduling.Source: C. Automated Theorem Proving · p. 3

III. PROSABUDDY

ProsaBuddy targets scarce training data and the long, dependency-rich proof contexts of schedulability analysis. It combines inference-time tool feedback, Prosa retrieval, optional human hints, and structured subgoal delegation.

A. Overview

  • Prosa’s limited volume relative to mathematics corpora constrains LLMs’ ability to learn schedulability-specific proof patterns.The paper describes Prosa as the main available resource for mechanized schedulability analysis.Source: A. Overview · p. 3
  • Schedulability lemmas can span hundreds of lines and depend on layered concepts, hypotheses, and preconditions tied to task-model assumptions.This length and conceptual depth burden context handling and reasoning.Source: A. Overview · p. 3
  • ProsaBuddy uses repeated proof attempts with external-tool feedback, Prosa retrieval for definitions and lemmas, and optional human hints for deep proof chains.These strategies address limits in pre-training domain knowledge and support navigation of difficult proofs.Source: A. Overview · pp. 3–4
  • A primary agent decomposes a Rocq lemma and sends subagents task bundles containing the subgoal, necessary context, and a proof-state snapshot.Agents retrieve from Prosa, use Rocq tools for feedback, and submit proofs for auditing.Source: A. Overview · p. 4

B. Lemma Decomposition

ProsaBuddy decomposes complex lemmas into subgoals for delegated proof, refining failed decompositions while preserving completed work. The decomposition is structured to be mechanically checked and guided by principles for producing locally solvable subgoals.

B. Lemma Decomposition

  • When a delegated subgoal fails, the primary agent can refine it into smaller subgoals while keeping those already proved, then recheck the composed proof.The process first decides whether to prove a lemma directly or decompose it; only terminal subgoals are delegated.Source: B. Lemma Decomposition · pp. 4–5
  • The primary agent checks decomposition structure by compiling a proof skeleton with each subgoal replaced by admit, ensuring the original lemma follows from the subgoals.Intermediate subgoals may be decomposed further; only terminal subgoals are dispatched to subagents.Source: B. Lemma Decomposition · pp. 4–5
  • Decomposition has high- and low-level stages: the agent does relatively well at high-level reasoning, especially with hints, but struggles to make low-level subgoals fine-grained enough.Manually written guiding principles target localized subproblems suited to solving in an isolated context.Source: B. Lemma Decomposition · p. 5

C. Proving Skills

ProsaBuddy derives reusable proving skills by analyzing proof traces and supplementing them with human review. The skills address recurrent proof difficulties, including applying lemmas whose many preconditions are hard to supply explicitly.

C. Proving Skills

  • Goal-management errors were the most frequent failures in the experiments, which the authors hypothesize may reflect LLM exposure to older Coq scripts rather than Rocq 9.x scripts.The passage attributes the hypothesis to explicit goal focusing and subproof bookkeeping in Rocq and newer SSReflect proof modes.Source: C. Proving Skills · p. 6
  • The final skill set contains 17 skills, generated from proof-trace candidates and then manually reviewed, filtered, and sometimes enhanced with human expertise.The traces came from attempts on 65 diverse Prosa lemmas using a preliminary system.Source: C. Proving Skills · pp. 5–6
  • For a lemma with many preconditions and parameters, using apply instead of exact turns them into goals that try done can close in the example.The exact approach requires explicitly supplying the full list, which the passage says is difficult for the LLM to provide correctly.Source: C. Proving Skills · pp. 6–7, Figure 5 · p. 7
  • Proving skills are generated from LLM analysis of traces followed by human review, whereas decomposition guidelines are written manually by experts.The authors report that trace-driven extraction of decomposition guidelines produced poor results, likely because decomposition effects are non-local and diffuse.Source: C. Proving Skills · p. 7

D. Tools

ProsaBuddy adds Rocq-aware tools for proof-state feedback, explicit proof planning, and detecting stagnation. These tools help agents work with structured proof information rather than relying only on raw command-line interaction.

D. Tools

  • Rocq tool wrappers provide whole-file compilation checks, queries about library objects and assumptions, and incremental diagnostics with current goals and hypotheses.The agent selects tools through OpenCode; the runtime dispatches calls and parses outputs into structured results.Source: D. Tools · p. 7
  • A planning tool represents decomposition as a DAG and checks target consistency, acyclicity, lemma applicability, and whether the resulting proof sketch compiles.It assigns delegated subgoals separate proof regions so subagents can edit their regions while preserving surrounding proof context.Source: D. Tools · p. 7
  • A stagnation tool compares Rocq states at proof milestones and warns or temporarily blocks attempts when repeated work on an unchanged region adds no new evidence.Progress records distinguish verified, structural, and diagnostic progress.Source: D. Tools · pp. 7–8

E. Proof Auditing

ProsaBuddy audits submitted proofs through compilation and checks that the proof body and surrounding file remain within allowed bounds. The audit relies on components beyond the Rocq kernel, and its soundness has not been formally verified.

E. Proof Auditing

  • A proof is accepted only if it compiles, its proof body contains only permitted proof-step or query commands, and changes outside the body are limited to initial trusted-library imports.Forbidden commands are detected in the proof-body AST; the original and submitted file ASTs are compared for changes outside the proof body.Source: E. Proof Auditing · p. 8
  • The audit runs in a separate OS process and rejects submissions that fail any check, but rejection is conservative and does not necessarily mean the proof is invalid.The authors state that the auditing procedure's soundness, including its design and implementation, has not yet been formally verified.Source: E. Proof Auditing · p. 8
  • The audit's assumed trusted base includes the Rocq kernel, compiler, allowed tactics, trusted libraries, astdump plugin, and auditing script.The audit inspects the AST rather than the proof term directly, so a bug in these components could cause an invalid proof to be overlooked.Source: E. Proof Auditing · pp. 8–9

A. Comparison with State-of-the-Art

On the 24-lemma benchmark, ProsaBuddy outperformed the compared systems; selected repeated runs and Prosa-library evaluations further supported its performance. These results concern lemmas connected to Prosa’s existing foundation, not real-time scheduling theorems in full generality.

A. Comparison with State-of-the-Art

B. Ablation Study

The ablations assess proving skills, lemma decomposition, human-written hints, and Prosa-library access. Each removed component reduced the number of proved lemmas, while decomposition and library access also affected token consumption.

B. Ablation Study

  • Without proving skills, ProsaBuddy proved 12 lemmas, fewer than the full system, supporting the contribution of the developed skills.Source: B. Ablation Study · p. 11
  • Without decomposition, the single-agent variant proved 14 lemmas; its gap from ProsaBuddy mainly appeared on harder cases, while planning and delegation sometimes increased token use.Source: B. Ablation Study · p. 11
  • Without human-written hints, ProsaBuddy proved 15 lemmas; hints mattered especially for difficult cases, while Prosa’s formal context already guided simpler proofs.Source: B. Ablation Study · p. 11
  • Without full Prosa-library access, ProsaBuddy proved 12 lemmas and often used more tokens, as it had to rediscover intermediate facts already available in the library.Source: B. Ablation Study · pp. 11–12
  • The evaluation also examined ProsaBuddy with different backbone LLMs, as reported in Table IX.Source: Table IX · p. 12

C. Different Backbone LLMs

GPT-5.4 yields ProsaBuddy’s highest reported proof count, while backbone choice substantially affects success; weaker models generally use more tokens on lemmas they prove.

C. Different Backbone LLMs

  • 17 lemmas with GPT-5.4, versus 9 with DeepSeek-v4-flash, 6 with DeepSeek-v4-pro, 2 with Gemini-3.1-flash-lite, and 1 with GPT-oss-120B.All components other than the backbone LLM were held constant.Source: C. Different Backbone LLMs · p. 12
  • DeepSeek-v4-flash unexpectedly proves more lemmas than DeepSeek-v4-pro, an anomaly the authors do not yet explain.They plan to investigate its cause in future work.Source: C. Different Backbone LLMs · p. 12
  • On the subset of lemmas weaker models prove, they tend to consume more tokens on average than GPT-5.4, with a few exceptions.Source: C. Different Backbone LLMs · p. 12
  • Table IX marks some experiments as omitted to save time and cost, because weaker models were thought likely to fail difficult cases that GPT-5.4 failed.Source: C. Different Backbone LLMs · p. 12

V. DISCUSSIONS AND CONCLUSIONS

ProsaBuddy is a preliminary system that proves many non-trivial lemmas, but the authors identify limits in evaluation and formalization support alongside directions for further development.

V. DISCUSSIONS AND CONCLUSIONS

  • ProsaBuddy successfully proves many non-trivial lemmas, but the authors characterize this work as preliminary, with limitations and room for further exploration.Source: §V · p. 12
  • In two ad-hoc cases, human-guided ProsaBuddy proofs took 2 and 3 hours, versus 14 and 17 hours manually; human-in-the-loop use was not systematically evaluated.The authors cite difficulty designing an objective, reproducible evaluation methodology for such interaction.Source: §V · p. 12
  • Lemma formalization remains a critical issue because no verifier can fully check whether it captures the intended meaning, motivating future LLM assistance.Source: §V · p. 12
  • The current decomposition guidelines and proving skills are only a small subset of possible additions, and may become obsolete as LLM reasoning improves.The authors envision users sharing skills that can be refined, reused, and benchmarked across projects.Source: §V · p. 12
  • Future work could explore combining ProsaBuddy with Proofreader, whose counterexample-seeking proof checks complement ProsaBuddy’s proof construction.The proposed joint use could accelerate theorem discovery, refinement, and validation.Source: §V · p. 12

Related papers

Loading 2610.03796v1…