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

cs.LOOct 1, 2026

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

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

Organizations: City University of Hong Kong · Northeastern University (China) · Northeast Forestry University · University of Electronic Science and Technology of China ·

Abstract

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

Figures & tables

Name	Source	Year	Prover	Availability
CoqPilot	[ 32 ]	2024	Coq	Yes
PALM	[ 33 ]	2024	Coq	Yes
COPRA	[ 34 ]	2024	Coq	Yes
Liu etc.	[ 35 ]	2024	Coq	No
Lu etc.	[ 36 ]	2025	Coq	No
Rango	[ 37 ]	2025	Coq	Yes

TABLE I: LLM-based automated Coq/Rocq theorem proving systems

Name	Brief Description
Reshaping	If an expression is mathematically useful but its exact form does not match what a downstream lemma requires, we should create a subgoal dedicated to reshaping the expression into the exact needed form. Example: If the context contains $\texttt{size (filter P xs)}\leq 1$ , a useful subgoal is to reshape it into $\texttt{count P xs}\leq 1$ , so that a counting lemma can be applied directly.
Witnessing	An object may already be known to exist, but it is still hidden inside an existential statement or an informal paper description. Then the proof should create a subgoal to make that object explicit and record the facts that come with it before using it in later steps. Example: When the context contains an existential fact about a job arriving in an interval I and belonging to task tsk , a useful subgoal is to extract a concrete witness j together with facts such as arrives_in j I and job_task j = tsk .
Library Matching	Prosa, MathComp, or local lemma may already be the right tool, but the current proof state is not ready for applying it. Then the proof should create a subgoal dedicated to preparing that lemma application: specializing general hypotheses to the current case, and writing out the required premises as explicit subgoals to be proved. Example: Suppose a Prosa lemma can prove the desired conclusion once it is given premises such as job_task j = tsk and arrives_in j I . A useful low-level decomposition is to create separate subgoals for these premises, prove them first, and then apply the library lemma directly.
Case Splitting	A proof may need to be split into cases, but each branch should not be packed into one big proof region. Then the proof should create a subgoal to make the case split explicit: write out the branch condition, and leave the rest of the branch proof to later subgoals. Example: We already know that the next step depends on whether a job j belongs to the set of jobs arriving in interval I , but we should have a subgoal dedicated to splitting j $\in$ jobs_arrived_during I , so that one branch explicitly carries the fact j $\in$ jobs_arrived_during I , and the other branch explicitly carries the fact j $\notin$ jobs_arrived_during I . Then the latter proof can handle the two branches separately, instead of hiding the whole case analysis inside one large proof step.
Lifting	When a goal concerns an set (e.g., counting, cardinality, or aggregation) but only per-element implications are available, introduce a subgoal to lift them to the set level. Example: If each job j that receives service in an interval I must have arrived before the end of I , a useful subgoal is to lift this fact to a counting inequality: count (fun j => receives_service_in I j) jobs $\leq$ count (fun j => arrived_before (end_of I) j) jobs .

TABLE II: Summary of Decomposition Guidelines

Fig. 3: An example of the decomposition-based proving procedure

Name	Brief Description
Small-step & inspect	Write one tactic at a time and inspect the resulting goal state after each step. This avoids writing long proof scripts without checking intermediate goals, and it helps keep the actual proof state in view.
Error priority	Resolve errors in priority order: syntax or parse errors first, then ill-typed terms, then unsolved goals or tactic failures, since later diagnostics are often consequences of earlier failures.
Tactic selection	Use simpler and more direct tactics before heavier or more search-based ones, such as reflexivity , lia , ring , tauto , congruence , auto / eauto , and decide / native_decide . For composite goals, decompose the goal first and automate each component separately.
Rewrite discipline	When rewrite fails because the rewritten term appears in dependent types, reorganize context with commands like generalize dependent or subst . Also, name small helper results with assert , pose proof , or set instead of packing too many steps into one long tactic chain.
Cleanup & final check	After a proof compiles, clean it up, choose deliberately between Qed and Defined , and then actually compile the file with a command such as coqc to make sure everything still works. A proof is not complete until temporary holes such as admit or Admitted. have been removed.
Syntax-driven rewrite	Before each rewrite, check whether the pattern required by the lemma already appears exactly in the current goal. If it does not, first transform the goal into that form instead of forcing the rewrite just because it seems mathematically correct.

TABLE III: Summary of Proving Skills

Classification	Operational role	Representative commands	Decision
VtProofStep	Advances or organizes the current proof state.	Tactic sentences, bullets, focusing commands and delimiters.	Allowed
VtQuery	Queries without modifying the interpretation state.	Check , Print , Search , Locate , and Show .	Allowed
VtStartProof	Initiates an interactive proof.	Lemma , Theorem , and proof-style Definition .	Forbidden
VtQed	Terminates or discards the current interactive proof.	Qed , Defined , Admitted , and Abort .	Forbidden
VtProofMode	Changes the proof mode used for subsequent proof commands.	Proof-mode switching commands, e.g., Proof Mode "Ltac2" .	Forbidden
VtMeta	Represents STM, history-management, or proof-control commands.	Back , Undo , Restart , and reset commands.	Forbidden

TABLE IV: Rocq command classifications [ 62 ] .

Index

# 1

# 2

# 3

# 4

# 5

# 6

# 7

# 8

# 9

# 10

# 11

# 12

# 13

# 14

# 15

# 16

# 17

# 18

# 19

# 20

# 21

# 22

# 23

# 24

Source

[ 63 ] Lem 3

[ 63 ] Lem 4

[ 63 ] Thm 6

[ 64 ] Thm 1

[ 64 ] Thm 2

[ 64 ] Thm 3

[ 64 ] Thm 4

[ 65 ] Lem 1

[ 65 ] Thm 1

[ 65 ] Lem 1-1

[ 65 ] Lem 1-2

[ 65 ] Lem 2-1

[ 65 ] Lem 2-2

[ 65 ] Lem 3

[ 65 ] Lem 4

[ 65 ] Lem 5

[ 65 ] Thm 1

[ 65 ] Thm 2

[ 66 ] Thm 3

[ 66 ] Lem 4

[ 66 ] Lem 5

[ 67 ] Lem 18.1

[ 67 ] Lem 18.6

[ 68 ] Lem 8

Dependency

# 1

# 1, # 2

# 3

# 8

# 10, # 11

# 12, # 13

# 14

# 15

# 16

# 21

# 20

# 22

num. of Tactics

70-110

160-200

180-300

10-40

70-90

10-40

60-80

30-70

200-220

150-200

40-60

15-30

10-20

100-150

20-80

15-90

60-80

TABLE V: Information of the Lemma in our Benchmark

Index

# 1

# 2

# 3

# 4

# 5

# 6

# 7

# 8

# 9

# 10

# 11

# 12

# 13

# 14

# 15

# 16

# 17

# 18

# 19

# 20

# 21

# 22

# 23

# 24

num. of success

PALM

✘

✔ 3

✘

RocqStar

✘

✔ 23

✘

✔ 587

✘

✔ 1,486

✘

AutoRocq

✘

✔ 6

✘

✔ 1176

✘

Cobblestone

✘

✔ 2

✘

OpenCode

✘

✔ 247

✘

✔ 1,083

✘

✔ 500

✘

PB-w/o-S

✔ 25,410

\bm{\infty}

✔ 23,440

✔ 206

✔ 3,760

\bm{\infty}

✔ 21,540

✔ 535

✘

✔ 45,185

\bm{\infty}

✔ 4,084

✔ 601

✔ 2,398

✔ 896

✔ 29,129

✘

TABLE VI: Results of the Comparison Experiments and Ablation Study with our Built Benchmark

Difficulty	Low		Medium		High
Index	# 15	# 17	# 8	# 22	# 1	# 2
PALM	0/5	0/5	0/5	0/5	0/5	0/5
RocqStar	0/5	1/5	0/5	0/5	0/5	0/5
AutoRocq	2/5	0/5	0/5	0/5	0/5	0/5
Cobblestone	0/5	0/5	0/5	0/5	0/5	0/5
OpenCode	0/5	2/5	0/5	0/5	0/5	0/5

TABLE VII: Results of Five Runs

	L1	L2	L3	L4	L5	L6	L7
num. of tactics	1-20	21-40	41-60	61-80	81-100	101-150	$>$ 150
PALM	1/10	0/10	-	-	-	-	-
RocqStar	7/10	2/10	-	-	-	-	-
AutoRocq	5/10	1/10	-	-	-	-	-
Cobblestone	1/10	0/10	-	-	-	-	-
OpenCode	4/10	0/10	-	-	-	-	-

TABLE VIII: Results with Lemmas Selected from Prosa

Index

# 1

# 2

# 3

# 4

# 5

# 6

# 7

# 8

# 9

# 10

# 11

# 12

# 13

# 14

# 15

# 16

# 17

# 18

# 19

# 20

# 21

# 22

# 23

# 24

num. of success

GPT-5.4

✔ 48,819

✔ 42,027

\bm{\infty}

✔ 13,332

✔ 281

✔ 1,295

✔ 2,077

✔ 13,077

✔ 1,888

✔ 24,330

✔ 36,004

✔ 38,749

✘

✔ 6,736

✘

✔ 3,908

✔ 2,229

✔ 307

✘

\bm{\infty}

✔ 31,614

✘

✔ 13,557

DeepSeek-v4-flash

\bm{\infty}

\bm{\infty}

\bm{\infty}

✔ 959

✔ 32,528

✔ 7,406

✘

✔ 4,013

\bm{\infty}

\bm{\infty}

\bm{\infty}

✔ 6,205

✔ 2,262

✔ 18,405

✔ 5,624

✔ 20,245

\bm{\infty}

DeepSeek-v4-pro

\bm{\infty}

\bm{\infty}

\bm{\infty}

✔ 2,201

\bm{\infty}

✔ 8,749

✘

✔ 4,247

✘

✔ 20,898

✔ 768

✘

✔ 4,567

✘

Gemini-3.1-flash-lite

✘

\bm{\infty}

\bm{\infty}

✔ 1,889

\bm{\infty}

\bm{\infty}

\bm{\infty}

✘

\bm{\infty}

✘

\bm{\infty}

\bm{\infty}

✘

✔ 10,355

✘

\bm{\infty}

GPT-oss-120B

✘

✔ 1,192

✘

TABLE IX: Experiment Results with Different Backbone LLMs

Automated Theorem Proving

Automated theorem proving develops algorithms and AI systems that construct or check formal proofs in mathematics, logic, and software.

See all 159 papers

PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs
Aug 13, 2026Sadat Shahriyar, Shareef Ahmed, Abdullah Al ArafatAutomated Theorem Proving Real-Time Scheduling
Florida International University · University of South Florida
TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents
Oct 10, 2026Kseniia Strelbytska, Balázs Szilágyi, Anna Mészáros +1Formal Verification Automated Theorem Proving
Stephen Perse Cambridge, UK · University of Cambridge, UK · Reasonable
Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification
Oct 7, 2026Shuangjie Yao, Nikolaus Holzer, Mark Paul Santolucito +3Automated Theorem Proving Formal Verification
Columbia University · The Hong Kong University of Science and Technology · Barnard College, Columbia University

Aug 13, 2026J/K move · Enter open · S save

PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs

Sadat Shahriyar, Shareef Ahmed, Abdullah Al Arafat

Florida International University · University of South Florida

Automated Theorem Proving Real-Time Scheduling LLM-Based Program Synthesis

Open paper AskPDF arXiv

Schedulability analysis is essential for certifying real-time systems, but existing tests are often developed through pen-and-paper proofs that are difficult to scale, validate, and maintain. Mechanized verification in PROSA/ROCQ offers a rigorous alternative, yet manually constructing such proofs requires substantial domain expertise and proof-engineering effort. Recent successes of large language models (LLMs) across a wide range of tasks make them promising candidates for generating PROSA/ROCQ scripts for mechanized theorem provers. However, state-of-the-art LLMs often lack the PROSA-specific knowledge required to correctly use its modeling abstractions and proof patterns. This paper introduces PROVE-RT, an LLM-assisted framework for generating PROSA/ROCQ scripts to mechanize schedulability analyses in real-time systems literature. PROVE-RT guides generation through dependency-aware informal sketches, retrieval from processed PROSA documentation, staged skeleton generation, and proof completion. We construct a mechanization-oriented corpus from 1, 191 real-time systems papers, containing 13, 134 informal sketches with dependency information. On a curated evaluation set, direct prompting of state-of-the-art LLMs fails to reliably generate valid PROSA mechanizations, whereas PROVE-RT achieves a success rate of 44.7%. These results show that retrieval-guided and staged LLM assistance can improve automated mechanization of schedulability analysis in PROSA/ROCQ.

Abstract

Automated Theorem Proving

Explore similar work

PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs

TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents

Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification