Paper deep dive
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
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%
Last extracted: 10/6/2026, 10:14:29 AM
Summary
The paper introduces ProsaBuddy, an LLM-based agent system designed to assist in mechanized real-time schedulability analysis using the Rocq proof assistant. ProsaBuddy addresses the high effort required for constructing machine-checkable proofs by employing a ReAct loop, retrieval over the Prosa codebase, and a subgoal-delegation architecture where a primary agent decomposes lemmas into subgoals for subagents. It outperforms existing LLM-based proving agents and general coding agents on benchmarks derived from real-time scheduling literature.
Entities (8)
Relation Signals (6)
ProsaBuddy → builton → OpenCode
confidence 95% · For these considerations, we build ProsaBuddy on top of OpenCode [8] rather than constructing an agent system from scratch.
PROSA → implementedin → Rocq
confidence 95% · It is built and verified using Rocq (formerly known as Coq) [6], a mature interactive theorem prover.
ProsaBuddy → targets → Rocq
confidence 95% · ProsaBuddy employs a ReAct loop with retrieval over the Prosa codebase, access to Rocq tools...
ProsaBuddy → uses → ReAct
confidence 95% · ProsaBuddy employs a ReAct loop with retrieval over the Prosa codebase...
ProsaBuddy → uses → subgoal-delegation architecture
confidence 95% · It uses a subgoal?delegation architecture, decomposing a lemma into subgoals and dispatches them to subagents for proof.
ProsaBuddy → outperforms → OpenCode
confidence 90% · Experiment results show that ProsaBuddy significantly outperforms state-of-the-art LLM-based Rocq automated proving agent systems and a general coding agent OpenCode.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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
Tags
Links
- Source: https://arxiv.org/abs/2610.03796v1
- Canonical: https://arxiv.org/abs/2610.03796v1
Trouble viewing inline? Open PDF directly →
Full Text
89,348 characters extracted from source content.
Expand or collapse full text
ProsaBuddy: Assisting Mechanized Real-Time Schedulability Analysis with LLM-based Agents Junyi Liu1,2, Tianchi Ren1, Fei Guan3, Xu Jiang4, Zhe Jiang5, Wang Yi6, Nan Guan1 Affiliation: Affiliation: 1City University of Hong Kong, 2Northeastern University (China), 3Northeast Forestry University, 4University of Electronic Science and Technology of China, 5Southeast University, 6Uppsala University 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 outperforms state-of-the-art LLM-based Rocq automated proving agent systems and a general coding agent OpenCode. †footnotetext: Junyi Liu and Tianchi Ren contributed equally to this work. Corresponding author: Nan Guan <nanguan@cityu.edu.hk> I Introduction In hard real-time systems, rigorous real-time performance analysis is essential to guarantee the system’s timing behavior to consistently meet specified constraints. Researchers in this field typically develop schedulability analysis theorems that provide efficient methods for evaluating real-time performance. The development of such analyses has traditionally relied on human effort and has been conducted in a pen-and-paper manner. However, numerous recent reports have revealed errors in schedulability analyses documented in literatures [1, 2, 3, 4]. Since real-time systems underpin safety-critical applications, such analysis errors can lead to disastrous consequences. Prosa [5] is an initiative that aims to fundamentally address this problem. Prosa provides a repository of definitions and proofs for mechanized (i.e., machine-checkable) real-time schedulability analysis. It is built and verified using Rocq (formerly known as Coq) [6], a mature interactive theorem prover. Prosa builds dedicated infrastructure and methodological frameworks to enable detailed, reliable, yet readable real-time schedulability analysis. Widespread adoption of the Prosa approach within the real-time systems research community would significantly elevate the rigor, credibility, and foundational robustness of theoretical developments in the field. Despite its potential, a practical barrier prevents Prosa from achieving broader adoption: developing proofs in Rocq is very time-consuming. Although Prosa has features that enhance its accessibility to real-time systems researchers, such as prioritizing readability and adhering to established proof conventions within the community, the overhead of proof development remains substantial. According to our own experience, proving lemmas in a real-time scheduling paper in Rocq based on Prosa may require several weeks, even for those with moderate familiarity with Prosa and Rocq. For newcomers without prior experience, it is even more demanding. This substantial effort is likely a primary factor discouraging researchers from adopting the Prosa approach in their own work. In this work, we present ProsaBuddy, an LLM-based agent system designed to lower the effort barrier to adopting the Prosa approach for developing mechanized schedulability proofs. While LLMs have demonstrated impressive automated theorem proving capabilities in domains such as pure mathematics, their application to theorem proving in real-time scheduling remains entirely unexplored. Although real-time scheduling lemmas can broadly be regarded as mathematical problems, they exhibit unique features that make them significantly more challenging to formalize and prove automatically than the pure-math problems in standard automated theorem proving benchmarks, as will be discussed in Section I-A. We build ProsaBuddy as an agent system that relies on inference‑time scaling through an intensive ReAct (Reasoning & Acting) loop [7]. It combines retrieval over the Prosa codebase to supply necessary definitions and proof patterns, access to various Rocq tools which provide rich feedback information, and optional human‑written proof hints that provide high‑level guidance. ProsaBuddy adopts a subgoal‑delegation architecture: a primary agent decomposes the lemma into smaller subgoals and dispatches them to subagents, each receiving a structured task bundle that includes the subgoal, context, and a proof state snapshot. We enhance the agents with decomposition guidelines and domain‑specific proving skills, improving their ability to navigate the deep proof chains. We conducted experiments to evaluate the performance of ProsaBuddy, comparing it with state-of-the-art LLM-based Rocq automated theorem proving systems, as well as a general-purpose coding agent OpenCode [8]. The comparison is conducted on a mini-benchmark of 2424 lemmas that we built from the real-time scheduling literature; none of them appear in the existing Prosa library. Experimental results show that ProsaBuddy significantly outperforms all competing systems. We further extend the evaluation to a larger set of lemmas taken directly from the Prosa library, and the results confirm the superiority of ProsaBuddy. Ablation studies reveal that these gains arise from the combined effect of several design choices in ProsaBuddy. Additionally, we assess the impact of different backbone LLMs on the performance of ProsaBuddy. Overall, ProsaBuddy successfully proves non-trivial schedulability analysis lemmas, including some whose Rocq proofs require hundreds of tactics. Nevertheless, we do not currently position ProsaBuddy as a replacement for human researchers or as capable of proving such lemmas entirely independently. Instead, ProsaBuddy is designed to liberate researchers from the tedious low-level details of lengthy Rocq proofs, saving them time to focus on developing high-level proof ideas. However, given the rapid development of LLMs, a vast open space remains for exploring whether ProsaBuddy could, in the future, assist real-time scheduling research in more advanced ways, for instance, by independently proving open problems or even automatically developing new theories. I Background and Related Work I-A Rocq Rocq (formerly known as Coq) is a proof assistant based on dependent type theory, allowing users to write mathematical definitions, executable algorithms, and prove properties about them interactively. Following the project’s renaming, we will refer to Rocq exclusively when introducing ProsaBuddy. One key difference between human‑written and Rocq proofs is the level of detail: a simple intuition often requires many explicit steps. For example, in the example of Figure 1, the lemma states that a job scheduled at time t cannot be completed by t. For humans, this is trivial. In Rocq, however, the proof needs many steps. So developing Rocq proofs is effort‑demanding. Rocq does not draw a fundamental distinction between Lemma, Theorem, Fact, or similar keywords – they all introduce a goal to be proved. In this paper, we will use the term lemma uniformly for any such goal to prove, regardless of which keyword was used in its declaration. A lemma statement in Rocq typically introduces variables, definitions, hypotheses, and a lemma statement. The proof is enclosed by Proof. and Qed., and the user guides the proof by applying tactics, which are commands that transform the current proof state (e.g., those marked in blue in Figure 1). Rocq provides a rich set of tactics, ranging from basic, primitive tactics that manipulate the proof state directly (e.g., move, rewrite, apply, exact) to powerful automation tactics that can search for proofs or solve decidable fragments automatically (e.g., auto, eauto, lia, ring). In the presentation of this paper, we deliberately minimize the reader’s dependence on understanding the syntax and semantics of Rocq. Our goal is to let readers who are not familiar with Rocq still grasp the key ideas, even if they skip some details. For some places that are key to understanding our methodology, we will introduce some tactics locally. For a comprehensive introduction to tactics mentioned in this paper, we refer the reader to the Rocq reference manual [9]. ⬇ 1 Context Job: eqType. 2 Variable job_arrival: Job → time. 3 Variable job_cost: Job → time. 4 Variable sched: schedule Job. 5 Context Task: eqType. 6 Variable job_task: Job → Task. 7 Definition scheduled_at (j: Job) (t: time) := sched t == Some j. 8 Definition service (j: Job) (t: time) := 9 _(0 <= t’ < t) scheduled_at j t’. 10 Definition completed_by (j: Job) (t: time) := 11 job_cost j <= service j t. 12 Hypothesis H_service_leq_job_cost: 13 forall j t, service j t <= job_cost j. 14 Lemma scheduled_implies_not_completed: 15 forall j t, scheduled_at j t → ~~ completed_by j t. 16 Proof. 17 move => j t. 18 rewrite /completed_by. move=> H_sched. rewrite -ltnNge. 19 have H_comp := H_service_leq_job_cost j (t + 1). 20 rewrite /service in H_comp. rewrite addn1 in H_comp. 21 rewrite big_nat_recr //= in H_comp. 22 rewrite H_sched /= in H_comp. rewrite /service. 23 by rewrite addn1 in H_comp. 24 Qed. Fig. 1: Example of a simple schedulability analysis lemma in Rocq I-B Prosa Prosa [5] is a Rocq-based foundation for verified real-time scheduling theory. It emphasizes readable specifications, explicit assumptions, and proof reuse. Following the SSReflect methodology [10], Prosa encodes its specifications as computable boolean predicates, which effectively enables proof automation via reflection. This clarity also makes Prosa well‑suited for LLM‑based proof automation, as its good readability is informative not only to human users but also to LLM. Prosa has been extended to verified scheduling infrastructure in several directions in follow‑up work, e.g., sustainability theory and weak sustainability [11], Abstract Response‑Time Analysis (ARTA) based on the busy‑window principle [12], FIFO response‑time analysis with arbitrary deadlines and arrival curves [13], and connections between response‑time analysis and network calculus [14]. Furthermore, Prosa serves as the certificate generator for POET [15], the first foundational response‑time analysis tool that produces fully machine‑checkable Coq/Rocq certificates. Another recent work integrates Prosa with RefinedC [16], connecting Prosa’s verified response‑time analysis with C implementation verification, thereby enabling end‑to‑end certification of interrupt‑free real‑time schedulers implemented in low‑level code. Together, these works make Prosa a useful infrastructure for verified real‑time systems. Nevertheless, Prosa currently focuses on a core subset of real‑time scheduling theory. I-C Automated Theorem Proving Mechanized proofs are inherently hard to construct. Before the emergence of LLMs, many efforts sought to improve automation for different theorem provers, for instance, via powerful tactics that search for proofs or solve decidable fragments automatically. For Coq/Rocq, SSReflect [10], Mathematical Components [17] and CoqEAL [18] enable reuse of recurring proof patterns through reflection and proof‑oriented computation; SMTCoq [19], smt4coq [20] and CoqHammer [21] connect Rocq goals to external solvers and reconstruct their proofs inside the kernel; Ltac/Ltac2 [22], Mtac/Mtac2 [23, 24], Coq‑Elpi [25] and MetaCoq [26] support domain‑specific tactics and reusable proof infrastructure. ML4PG [27], CoqGym [28], Tactician [29], Proverbot9001 [30], TacTok [31] and ASTactic [28] explored proof‑pattern mining, tactic prediction, local proof search, and proof‑step prediction. These techniques substantially reduce routine proof effort, but they do not fully eliminate the high demand for expert intervention. Large mechanized developments still require experts to decompose complex goals, formulate auxiliary lemmas, choose suitable abstractions, and coordinate induction arguments. TABLE I: LLM-based automated Coq/Rocq theorem proving systems 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 ADAPT [38] 2025 Coq No RocqStar [39] 2026 Rocq Yes Cobblestone [40] 2026 Coq Yes AutoRocq [41] 2026 Rocq Yes ReCent-Prover [42] 2026 Rocq No QUARRY [43] 2026 Rocq No LLMs have recently been used for automated theorem proving across several proof assistants. Existing work has been done for different theorem provers, including Coq/Rocq [32, 34, 33, 37, 39, 42], Lean [44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54] and Isabelle/HOL [55, 56, 57]. In the following, we focus on the work for Coq/Rocq, and refer to recent survey papers [58, 59] for a more comprehensive overview of the field. CoqPilot [32] provides a Coq-oriented assistant implemented as a VS Code extension, where users mark proof holes with admit, configure completion services, and invoke the tool inside an open Coq file to generate, check, and substitute candidate proofs through coq-lsp during interactive editing. COPRA [34] formulates proof search as an in-context interactive process where the model proposes tactics and observes proof-state feedback. PALM [33] uses a generate-then-repair architecture to analyze and repair low-level proof errors. More recent systems combine proof generation with retrieval and multi-step interaction. Rango [37] retrieves relevant premises and similar proofs from the current Coq project. RocqStar [39] and ReCent-Prover [42] further introduce planning, reflection, and strategy-aware retrieval into Rocq proof generation. Recent systems also enrich proof context and refine failed proof attempts. Lu et al.[36] use selective concept unfolding and separate proof planning from tactic generation. Liu et al.[35] explain terms in proof obligations and repair incomplete tactic parameters. ADAPT [38] selects among different refinement strategies after a failed proof attempt. QUARRY [43] ranks candidate sublemma decompositions by their estimated CoqHammer solvability. Cobblestone[40] retains Coq-accepted subproofs and recursively processes failed parts, while AutoRocq[41] combines proof-tree context, Rocq feedback, and previous proof attempts for software verification. Table I lists existing LLM-based automated Coq/Rocq theorem proving systems. Overall, this body of work shows a shift from isolated tactic prediction to systems combining proof synthesis, retrieval, prover feedback, repair and agentic control. However, proofs in real-time scheduling often rely on recurring semantic structures, including scheduling assumptions, workload and processor models, invariants, response-time bounds, rewriting conventions, and sequences of lemmas. Existing methods treat reusable knowledge as retrieved premises, similar proofs, or short-term proof-state contexts. They do not make domain-specific proof procedures explicit as reusable skills with applicability conditions, required assumptions, expected effects and adaptation strategies. This leaves a gap between general LLM-based proof generation and domain-aware proof automation. I ProsaBuddy I-A Overview Before presenting our approach, we first discuss the major differences between the problem tackled in this paper, automated theorem proving for real‑time schedulability analysis, and the more commonly studied application of LLM‑based automated theorem proving to pure mathematics. The theorem-proving capability of LLMs is obtained via pre‑training on large‑scale corpora such as Mathlib [60]. In contrast, public data for mechanized schedulability analysis is very limited. The Prosa library is the main available resource, but its volume is orders of magnitude smaller than the corpora for mathematics. This scarcity fundamentally constrains the ability of LLMs to learn proof patterns specific to the schedulability analysis domain. The schedulability analysis lemmas are substantially more complex than those found in mathematics benchmarks. They are built upon a complex hierarchy of concepts, requiring many intricate definitions that often recursively depend on one another across multiple levels, along with numerous hypotheses. For example, in the PutnamBench suite [61] for evaluating LLM-based mathematics theorem proving, the description of a lemma spans no more than 2020 lines. In contrast, the complete description of a schedulability analysis lemma in Prosa, including all definitions, variables, assumptions, and the lemma itself, often extends to several hundred lines. This increased length and conceptual depth impose a significantly heavier burden on LLM’s context handling and reasoning capabilities. Beyond the complexity of individual lemmas, Prosa has a highly structured architecture that promotes lemma reuse across different task models. Whether an existing lemma can be applied to prove a target lemma depends on whether its preconditions hold, and those preconditions, in turn, rely on further preconditions, ultimately tracing back to the specific assumptions of the task model under consideration. This unique feature has introduced extra difficulty in the proving. We will further elaborate on this point in Section I-C. To address the above challenges, ProsaBuddy adopts several complementary strategies. First, because pre-training cannot supply sufficient domain knowledge, we rely on inference-time scaling: the LLM repeatedly attempts the proof, using feedback from external tools. Second, we leverage the existing Prosa library to retrieve relevant definitions and lemmas, and to learn proving techniques by imitating how Prosa handles similar problems. This demands a powerful retrieval capability capable of accurately locating useful information within Prosa. Third, we incorporate optional human-provided proof hints, which help the agent navigate deep proof chains that would otherwise be difficult to resolve automatically. For these considerations, we build ProsaBuddy on top of OpenCode [8] rather than constructing an agent system from scratch. OpenCode provides a solid foundation that satisfies the requirements outlined above. In OpenCode, an agent follows an iterative ReAct (Reasoning & Acting) loop [7]: it queries the LLM, uses the reasoning in the model’s output to execute external tools, and then appends the feedback to the conversation context for the next query, repeating this process until the task is resolved. OpenCode offers powerful code search capabilities well-suited for retrieval over the Prosa library and allows users to inject human-written proof hints into the agent’s prompt easily. By building on OpenCode, we inherit a mature agent foundation and can focus our efforts on developing high-level capabilities tailored to the needs of schedulability analysis lemma proving. Figure 2 shows the major components of ProsaBuddy. The system takes as input a lemma formalized in Rocq, along with optional human-written proof hints. The output is a verified proof in Rocq, or a failure declaration. For proof construction, ProsaBuddy uses LLM-based agents in a subgoal-delegation architecture. The primary agent decomposes the lemma into smaller, independent subgoals and dispatches them to specialized subagents. The subagent leverages OpenCode’s existing infrastructure, which already supports launching subagents. When launching a subagent, the system does not simply forward the original prompt. Instead, it builds a structured task bundle that includes the subgoal to prove, the necessary context, and a snapshot of the current proof state, for the subagent to solve the assigned subgoal independently. We detail the lemma decomposition process in Section I-B. The agents retrieve relevant information from the Prosa codebase using OpenCode’s standard file-reading and code-search tools, such as file browsing and grep-like search. Beyond these standard capabilities, we enable ProsaBuddy to invoke Rocq tools directly to get rich feedback information for its ReAct loop. We elaborate on these external tools in Section I-D. We also equip the agents with a collection of proving skills that target common challenges in the proving procedure, which will be elaborated in Section I-C. Last but not least, the proof submitted by the agents must go through auditing before it is finally accepted as a valid proof of the target lemma, which will be introduced in Section I-E. Fig. 2: Overview of ProsaBuddy I-B Lemma Decomposition TABLE I: Summary of Decomposition Guidelines 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 size (filter P xs)≤1 size (filter P xs)≤ 1, a useful subgoal is to reshape it into count P xs≤1 count P xs≤ 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 ∈ jobs_arrived_during I, so that one branch explicitly carries the fact j ∈ jobs_arrived_during I, and the other branch explicitly carries the fact j ∉ 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 ≤ count (fun j => arrived_before (end_of I) j) jobs. Fig. 3: An example of the decomposition-based proving procedure The proving process starts with the primary agent, which first decides whether the lemma to be proved is simple enough to be proven by itself; if so, it attempts to complete the proof directly. If the lemma is complex, it performs lemma decomposition, i.e., breaks the target lemma into several subgoals. Each subgoal is then delegated to a subagent for proof. After launching a subagent, the primary agent suspends and waits for that subagent to return. The subagent returns to the primary agent with either a success or a failure, accompanied by a failure report that explains why it failed and what important piece of information is missing for it to complete the proof of that subgoal. Upon receiving a failure return from a subagent, the primary agent attempts to refine the decomposition. When the primary agent refines the decomposition, all subgoals that have already been proved will be kept. Figure 3 shows an illustrative example of the proving process. The primary agent first decomposes the target lemma into two subgoals, A and B. The subagent proving A returns with a success, but the one proving B returns with a failure. The primary agent then analyzes the failed subgoal, redo the decomposition, further divides subgoal B into smaller subgoals C and D, and dispatches them to subagents for proof. Once both C and D are successfully proved, the primary agent performs a final recheck to ensure that all generated proofs returned from the subagents compose into a valid proof of the original lemma. The decomposition by the primary agent is mechanically checked for structural correctness: it guarantees that the original lemma follows from the conjunction of the subgoals. Concretely, the agent constructs a proof skeleton in which each subgoal is replaced by admit, and then verifies that this proof is accepted by the Rocq compiler, as illustrated in Figure 4. Nested decomposition is permitted (e.g., introducing a have tactic within another have, provided it reflects a genuine sub-step or a structural refinement of the reasoning). Intermediate subgoals (those that are further decomposed) are not delegated to subagents; only terminal subgoals (those that are not further decomposed) are delegated to subagents for proof. In Figure 4, the original lemma T is decomposed into H1 and H2, where H1 is an intermediate subgoal and H2 is terminal. H1 is further decomposed into the terminal subgoals S1 and S2. The terminal subgoals S1, S2 and H2 are then dispatched to subagents for proof. ⬇ 1 Lemma T (a b c d e : nat) : 2 a + c <= b + d. 3 Proof. 4 have H1 : a <= b. 5 6 have S1 : a <= e. 7 admit. 8 have S2 : e <= b. 9 admit. 10 exact: leq_trans S1 S2. 11 12 have H2 : c <= d. 13 admit. 14 exact: leq_add H1 H2. 15 Admitted. Fig. 4: An example of the proof script for lemma decomposition The primary agent performs lemma decomposition in two stages. First, a high-level decomposition stage reasons about the current context (incorporating any human-written proof hint, if given) to extract fundamental steps that can genuinely advance the proof. Second, a low-level decomposition stage transforms those high-level steps into a proof skeleton directly provable in Rocq. It turns out that the agent is doing relatively well with the high-level decomposition, especially when human-written proof hints are given. However, the agent struggles in the second stage. Because the low-level decomposition relies on the backbone LLM’s inherent reasoning capability, it is usually not fine-grained enough, and thus the resulting subgoals are difficult for the subagent to prove. To solve this problem, we further augment the agent with extra guiding principles that are extracted manually from our experience in using Rocq for theorem proving. These principles provide instructions tailored to situations where low-level decomposition is effective (summarized in Table I). Specifically, they target highly localized sub-problems that are largely independent of the surrounding proof, making them ideal for a subagent to solve in a clean, isolated context. The guiding principles are embedded in the main agent’s prompt. The full prompt is considerably more detailed, and Table I gives only a brief overview. I-C Proving Skills TABLE I: Summary of Proving Skills 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. Local bridge lemmas Use a small local bridge lemma when the mismatch is specific to the current branch or to a fixed local expression. Extract a generic lemma only when the same normalization gap recurs across proofs. Minimal expansion When a by fails, remove by and keep the rest exactly the same. Re-run immediately and record both the first revealed error message and the number of focused goals. If expansion produces multiple goals, the primary issue is proof structure. If it reveals a rewrite mismatch, the issue is the current goal shape. If it reveals Cannot apply or No assumption, the issue lies in the lemma preconditions or the local context. Expand “by” patterns Expand compressed forms such as by rewrite, by apply:, have …by …, and case …; by … into ordinary proof scripts so that you can see exactly which step fails or which branch is still open. After expanding one by step, fix only that step. Do not guess new tactics before reading the first real error, and shorten it back to by only after the expanded version is confirmed to close the proof correctly. Bool/Prop boundary If the remaining reasoning is easier to carry out in Prop than in Boolean form, convert the comparison once and finish the branch in Prop, reflecting back only if the final goal is Boolean. Normal form & bridge order First decide what form the final result should have: a count expression or a big-operator expression. After choosing that target form, rewrite in one direction: indicator sum -> filtered big operator -> count. Do not switch back and forth between forms. Big-op normalization order First simplify the innermost sums that are easy to evaluate, such as constant sums or sums of Boolean tests. Then reorganize the outer sum if needed. Only after that should you rewrite repeated addition as multiplication. Try to keep the whole branch in one consistent form instead of repeatedly switching between sums, iter, and multiplication. Count before min First rewrite the main counting fact into a clear bound on count, such as count P s <= k. Only after that should you handle Nat.min, minn, or the final arithmetic inequality. Do not start the final arithmetic steps while the same quantity is still written in several different counting forms. Failure signals If big_mkcond or sum1_count does not apply, the expression is usually still in the wrong form. A common mistake is to skip the intermediate normalization steps and jump straight from an indicator sum to count or even to a min inequality, which makes both the rewrites and the later arithmetic harder to control. Failure signatures When rewrites such as mul1n, mulnC, or big_ord_recr fail, the expression is usually still in the wrong form. If the branch has become a counting problem involving count, sum1_count, or Nat.min, switch to the count-normalization skill instead of continuing with generic big-operator rewrites. Goal management Use this skill when a Coq or Ssreflect proof has drifted into a multi-goal state after a branching tactic or local sublemma, especially when coqc reports “Expected a single focused goal but 2 goals are focused,” and the next step should be structural recovery with bullets, braces, and explicit branch closure rather than further mathematical reasoning.1 Goal-driven lemma instantiation This skill helps distinguish between ordinary subgoals that can be proved later and early parameters or prerequisites that Coq must know immediately. It recommends using apply or eapply to let the current goal expose the real remaining obligations, and, if necessary, supplying only the first missing parameter or preconditions instead of writing a long, fully explicit exact term. 1 Goal-management errors were the most frequent failures in our experiments. This is likely because Rocq and newer SSReflect proof modes enforce goal focusing and subproof bookkeeping more explicitly, so compressed proof scripts that worked in older Coq settings may fail in Rocq. We hypothesize that current LLMs have seen more older Coq scripts than Rocq 9.x scripts, and therefore often generate fragile goal-management patterns that lead to these errors. We develop proving skills to enhance the subagent’s ability to prove delegated subgoals. These skills are generated by using the LLM to analyze the proving traces, using the following process. First, we select 6565 lemmas from Prosa (only a small fraction of Prosa) as training lemmas11 1 For detailed information on the training lemmas, see the ProsaBuddy Github repository ⟨ ://github.com/ProsaBuddy/RTSS2026⟩ .. The selection criteria aim for diversity: we choose lemmas with proofs that vary in tactic count (i.e., difficulty), and we sample from different files and, whenever possible, different subdirectories within the Prosa codebase. We use a preliminary version of our system (equipped with external Rocq tools and the Prosa codebase) to attempt to prove these lemmas, and we collect the full traces of the proving procedure. Each trace captures the agent’s iterative attempts, including failures, error messages, and proof states, until success. We then fed these traces to an LLM to analyze failure reasons and generate skills. Concretely: 1. We use LLM to divide each trace into segments, each handling a local task (e.g., fixing an error in the proof). 2. For each segment, we use the LLM to identify the problem being solved, analyze its cause, and generate a skill to avoid or resolve it. This produces a pool of proving skill candidates. 3. We use the LLM to merge proving skill candidates that address the same or similar problems. 4. Finally, we manually review the remaining candidates, discarding those that are too general, vague, or lacking useful information, and enhance some of them with human expertise. This results in the final 1717 proving skills as summarized in Table I. ⬇ 1 exact (@uniprocessor_response_time_bound_restricted_supply_seq 2 Task H (@limited_preemptions_rtc_threshold Task H H1) 3 Job H2 H4 H3 (@limited_preemptive_job_model Job H5) 4 PState H_uniprocessor_proc_model H_unit_supply_proc_model 5 H_consumed_supply_proc_model arr_seq VALID_ARRIVALS 6 sched JOBS_FROM_ARRIVAL_SEQUENCE JOBS_MUST_ARRIVE 7 COMPLETED_JOBS_DONT_EXECUTE VALID_COSTS ts tsk H_tsk_in_ts 8 VALID_PREEMPTION_MODEL VALID_RTCT H0 VALID_ARRIVAL_CURVE 9 RESPECTS_MAX_ARRIVALS 10 (rs_jlfp_interference arr_seq sched) 11 (rs_jlfp_interfering_workload arr_seq sched) 12 ABSTRACT_WORK_CONSERVING H_sequential_tasks 13 I_AND_W_SEQUENTIAL 14 L BUSY_INTERVALS_BOUNDED (arm_sbf Π Θ ν) 15 INTRA_BOUNDED R SOL_SEQ_RS 16 j ARR TSK). ⬇ 1 apply : uniprocessor_response_time_bound_restricted_supply_seq; 2 try done. Fig. 5: Example illustrating the goal-driven lemma instantiation proving skill. The upper part shows the proof script using exact, i.e., explicitly providing all the needed preconditions and parameters. The lower part shows the proof script using apply combined with try done. Due to space limitations, we cannot elaborate on every proving skill in Table I. In the following, we only give a detailed explanation of the goal-driven lemma instantiation proving skill (the last row in Table I), which addresses a problem specific to schedulability analysis using Prosa. As mentioned in Section I-A, Prosa has a highly structured hierarchy that facilitates lemma reuse across different task models. Applying such a lemma requires satisfying its preconditions, which themselves depend on further preconditions, eventually reaching the specific assumptions of the chosen task model. In these cases, the agent tends to use the exact tactic when applying such lemmas, which requires all preconditions and parameters to be explicitly supplied. The upper part of Figure 5 shows a real example we take from the traces for generating the proving skills. In this example, the lemma requires a long list of preconditions and parameters (lines 2 - 16) if using exact to apply this lemma. It is very difficult for the LLM to precisely provide all the required preconditions and parameters. Even if the agent repeatedly guesses parameters, receives error messages from Rocq tools, and tries again, in most cases, it still can never find the correct combination. However, a simple solution exists for this problem: instead of using exact with all parameters, one can use the apply tactic with the lemma. This turns the preconditions and parameters into explicit goals, which are typically much easier to prove (many can be resolved automatically by built-in tactics). For instance, the lower part of Figure 5 shows the proof script that applies the lemma using apply, without providing the preconditions, and then using try done can close all the generated goals. This insight becomes a reusable proving skill. Why does analyzing proof traces enable the LLM to generate useful skills? The traces contain rich diagnostic information: they show iterative attempts to solve a local problem, with clear success/failure outcomes, error messages, and the current proof state at each step. The LLM can observe how the agent fails repeatedly and how it eventually succeeds. The resulting proving skill thus encodes a practical solution that the LLM alone would not produce. TABLE IV: Rocq command classifications [62]. 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 VtSideff May modify the global environment, parser state, or interpretation state. Axiom, Parameter, Definition, Require, Notation, Set/Unset, Hint, Instance, and Declare ML Module. Forbidden It is worth comparing proving skills with the decomposition guidelines. Both serve the same purpose: adding extra information to the LLM’s prompt to improve its problem-solving ability. The differences lie in how they are obtained and used. Decomposition guidelines are crafted manually by human experts, while proving skills are generated by having the LLM analyze proof traces, followed by human review. We also attempted to use a similar trace-driven process to extract decomposition guidelines, but the results were poor. This is probably because the impact of a decomposition is non-local and diffuse; the LLM struggles to connect later proof failures to decomposition choices and infer how the decomposition should be refined. Moreover, while proving skills are stored in skill files and loaded on demand, decomposition guidelines are placed directly in the agent’s prompt. The current set of decomposition guidelines is small, so the benefit of making them load-on-demand is limited, but nothing prevents users from packaging them as on-demand skill files. I-D Tools In addition to the standard built-in tools in OpenCode, such as file reading and code search, we develop several extra tools to assist the proof construction. We integrate a suite of Rocq tools that supply fine-grained, context-aware feedback based on the current proof state. Rocq provides a batch compiler and an interactive toplevel, i.e., a REPL (read–eval–print loop). rocq-lsp is a separate language server/plugin for Rocq. Our tools wrap these underlying interfaces. We develop a compiler-backed tool that checks whole .v files and reports compilation status and errors, a toplevel-backed tool that answers queries about library objects, lemma types, assumptions, and definitions, and a rocq-lsp-backed tool that provides incremental diagnostics, current goals and local hypotheses. Our integration follows OpenCode’s standard way of providing tools. Each tool is a module with a call name, a brief description, and an input schema. The agent does not run Rocq directly. It selects a tool and supplies arguments, and the OpenCode runtime dispatches the call, using session configuration such as file paths and project roots. The output is written to files, which the OpenCode harness parses into structured results such as error locations, goals, and hypotheses. This gives the agent fine-grained proof-state feedback while avoiding fragile raw command-line handling. We developed a structured proof-planning tool that enables the primary agent to externalize its decomposition as an explicit DAG before constructing a proof sketch that can be compiled by Rocq. Each node in the DAG records a Rocq subgoal, its dependencies, and optionally proposed library lemmas; terminal delegation candidates are materialized as annotated proof regions. The tool mechanically checks target-lemma consistency, acyclicity, and lemma applicability, and compiles the resulting sketch to ensure the subgoals can be combined. It also assigns each delegated subgoal a unique proof region, so a subagent can edit only its assigned region while preserving the surrounding proof and local context. This tool is useful since, if a decomposition remains only in the primary agent’s free-form reasoning, invalid decompositions may go unnoticed until subagents fail. We also developed a tool to detect stagnation in proof construction. Since the Rocq compiler reports only the current proof state, it cannot determine whether repeated agent actions are advancing the proof or reproducing the same failure; without an independent progress assessment, the agent may keep calling the same tools, launching subagents on unchanged proof regions, or making superficial edits while wasting computation and tokens. At proof milestones, such as after the primary agent writes or substantively revises a proof sketch, after a proof region is updated, or after a subagent returns, the tool invokes Rocq, compares the new state with the previously recorded one, and records verified, structural, or diagnostic progress. It then uses these records to detect stagnation: if repeated tool calls or subagent attempts on an unchanged region produce no new evidence, it warns the agent and may temporarily block further attempts until new compiler evidence appears or the region’s subgoal, dependencies, or proof commands are substantively revised. I-E Proof Auditing When an agent declares a proof complete, we cannot treat that declaration, or even a successful compilation, as evidence that the proof has actually been written, since the agent may “cheat” during proof construction. For example, an agent might silently change the theorem statement, weaken a definition, or introduce an unproven axiom. This could still result in a successful compilation, yet not give a valid proof of the intended lemma. We therefore need an independent auditing step to decide whether the proof is valid. The goal of proof auditing is to ensure two things: (1) the lemma to be proved is unchanged, and (2) the generated proof indeed proves the lemma rather than bypassing its proof. ProsaBuddy runs in a sandbox, an isolated workspace that limits which files the agent can read and write. We place the libraries the agent is allowed to use in its read-only scope, so that the agent can import from them but cannot modify or recompile the libraries themselves. Based on this, the auditing consists of the following steps. First, we check whether the submitted .v file, which contains the lemma to be proved and its proof script, is accepted by Rocq. Concretely, this means that when the Rocq compiler processes the file, it is parsed and elaborated without errors, and the proof terms produced by the tactics are accepted by the Rocq kernel. In particular, if the proof script contains tactics that leave unfinished goals, such as admit or give_up, the check fails at this step. Second, we check that the proof body, i.e., the part after Proof. and before Qed., contains only commands for advancing or querying the proof state. Table IV shows the classification of Rocq commands. Among these classes, only the VtProofStep and VtQuery classes are allowed in the proof body; all other classes are forbidden. We use the astdump plugin (part of rocq-lsp) to extract the AST of the .v file and check whether there is an AST node corresponding to a command in a forbidden class within the proof body. If so, the check fails at this step. Third, we verify that nothing outside the proof body has been changed, except for imports from trusted libraries at the very beginning. Specifically, before the agent starts working, we store a copy of the original .v file containing the target lemma. After the agent submits its .v file, we compare the ASTs of the two files to ensure that any changes outside the proof body are limited to imports from trusted libraries at the very beginning; otherwise, the check fails. Currently, we treat only MathComp and Prosa as trusted libraries and assume that importing them at the beginning of the .v file does not introduce risks of altering the lemma to be proved or enabling the agent to bypass the proof. A proof submitted by the agent is deemed valid only if it passes all the steps above. Otherwise, the submitted proof is rejected and returned to the agent for reconstruction. Note that the audit is performed in a different OS process, so any changes to the Rocq environment state made by the proving agents cannot affect the Rocq environment state used in the audit. The above auditing procedure is conservative in the sense that a proof file submitted by the agent is not necessarily invalid just because it failed the audit. Nevertheless, the soundness of our proof auditing, both its design and implementation, has not yet been formally verified. Establishing a formally verified proof auditing procedure will be our future work. Besides our proof-auditing script itself, we rely on several trusted bases to declare a proof valid. The scope of the trusted base depends on the property being checked. For kernel-level proof validity, the trusted base is the Rocq kernel: it is the component that actually checks proof terms, and Rocq is designed so that nothing else needs to be trusted for soundness. ProsaBuddy’s proof-auditing procedure, however, relies on additional components. Our assumed trusted base for auditing consists of the Rocq kernel, the Rocq compiler, the tactics allowed to be used, the trusted libraries, the astdump plugin, and our proof-auditing script. Trust to these components is needed because our audit does not inspect the proof term directly. It inspects the AST and checks whether the AST contains forbidden commands. The absence of such commands in the AST, however, does not by itself guarantee that the proof term submitted to the kernel is free of them. The AST is extracted from the source file by the astdump plugin, and the proof term is obtained by compiling the source file, during which the tactics are executed. To infer from the absence of forbidden commands in the AST that the proof term is also free of them, we have to trust the astdump plugin, the compiler, the tactics and the imported libraries, as well as our proof-auditing script. A bug in any of these components might cause our auditing procedure to overlook an invalid proof, even though the Rocq kernel itself remains sound. However, the tools that agents use while generating proofs need not be trusted: they are used only to provide information guiding agents to construct proofs, and the correctness of this information does not affect the auditing procedure. IV Evaluation IV-A Comparison with State-of-the-Art We compare ProsaBuddy with four recent LLM-based automated theorem proving systems for Coq/Rocq: PALM [33], AutoRocq[41], Cobblestone[40] and RocqStar [39]. The interaction layer with Coq of PALM and Cobblestone relies on coq-serapi, which has only been maintained up to Coq 8.20. This dependency prevents PALM from being directly applied to the Rocq environment. Since our experiments use Rocq 9.0 for RocqStar and ProsaBuddy, we ported the subset of coq-serapi interaction functionality used by PALM to Rocq 9.0 for a fair comparison. We also attempted to evaluate COPRA [34], another recent LLM-based Coq/Rocq proving agent, but COPRA failed on all benchmark tasks in our environment; therefore, we do not include its results in Table VI. We investigated the failures and found that, although COPRA claims support for both Lean and Coq, the released GitHub implementation leaves several Coq-environment connection functions unimplemented. We did not compare with Rango [37] because RocqStar has already included a direct comparison with Rango and reported better performance [39]. Therefore, we only choose the better one as the representative baseline in our experiments. We did not compare with CoqPilot because RocqStar is a follow-up system that extends the CoqPilot pipeline with a more advanced agentic architecture [32, 39]. We did not compare with ADAPT[38], QUARRY[43], ReCent-Prover [42] and the work in [35] and [36] because they are not yet publicly available. Moreover, we also include the original OpenCode in the comparison. For all systems, we use GPT-5.4 as the backbone LLM. All compared systems have access to the full Prosa library. 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 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 #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 Note: “Dependency” represents which other lemma in this table are prerequisites for this lemma. “# of Tactics” represents the range of the number of tactics in the proof generated by different systems in the following evaluation experiments (different systems often generate proofs with different numbers of tactics). For those lemmas/theorems which are not proved by any system, the number is denoted by “-”. The evaluation is conducted on a benchmark that we created. The benchmark contains 2424 lemma formalizations in Rocq, which are not included in the existing Prosa library. These lemmas are drawn from five research papers [63, 64, 65, 68, 66] and one book [67] in real-time scheduling theory, and we manually formalized them in Rocq. This ensures that the benchmark has no overlap with the “training” lemmas used to automatically generate the proving skills, as introduced in Section I-C. The sources of these lemmas are listed in Table V. All lemmas concern global multiprocessor scheduling. Note that, in Table V, case #10 and #11 (and also #12 and #13) come from manually splitting a single lemma into separate smaller lemmas. We do this when the original lemma states multiple independent results at once. This does not change the mathematical content of the original result. There is a compatibility issue: Prosa 0.4 includes foundations for global multiprocessor scheduling, but the latest version, Prosa 0.6, does not have this part. Prosa 0.6 is based on Rocq, whereas Prosa 0.4 is based on Coq, and Rocq and Coq have subtle syntactic differences. Therefore, we manually ported the global multiprocessor scheduling part in Prosa 0.4 from Coq to Rocq. We use the relevant portion of the corresponding research paper as the human-written proof hint input. Specifically, this input includes the target theorem or lemma itself, its full human-written proof, as well as any supporting definitions, notation, and variables that are referenced within the proof. AutoRocq, OpenCode and ProsaBuddy accept this input through their existing interfaces. However, PALM, Cobblestone, and RocqStar do not originally provide such an interface. PALM and Cobblestone operate through their generate-and-repair workflows, which take the formal lemma and the current proof state as inputs and iteratively attempt to construct a valid proof. Neither PALM nor Cobblestone accepts additional text inputs. RocqStar retrieves formal definitions and theorems from a structured Rocq library, but it does not accept free-text descriptions as input. To provide the same human-written proof hint to all systems, we augmented PALM, Cobblestone, and RocqStar to prepend the corresponding hint to their system prompts. All comparison results reported for PALM, Cobblestone, and RocqStar are obtained from their augmented version with human-written hints. Table VI shows the comparison results. Each column in the table is the lemma index in the benchmark. In each cell, ✔ represents that the lemma is successfully proved, while ✘ represents the agent declares a failure to prove this lemma and stops. The number under ✔ represents the total amount of token consumption proving this lemma in the unit of 11K tokens (counting both input tokens and output tokens). ∞ ∞ represents that the agent has not yet proved the lemma before reaching the timeout threshold. In our experiments, we set the timeout threshold to be 50,00050,000K tokens. The timeout is measured by the number of tokens consumed rather than by actual time consumption, since variations in time delay depend heavily on many factors unrelated to the model inference, such as network latency, server load, or local hardware restrictions. In contrast, the token count provides a more stable metric that better reflects the amount of LLM inference performed. To give readers a rough sense of scale, in most cases ProsaBuddy takes between 33 and 55 hours to reach the 50,00050,000K‑token threshold. Besides the total token consumption, the KV-cache hit rate is also a key factor determines the proving efficiency and cost. The KV-cache hit rate of ProsaBuddy is on average about 90%90\% in our experiments22 2 The KV-cache hit rate also depends on the LLM serving provider’s KV-cache resource allocation policy. For example, the KV-cache hit rate will drop if less KV-cache space is allocated to each request session. Therefore, this KV-cache hit rate result may not be reproducible.. To reduce time and cost, we omit some experiments, which are denoted by “–” in Table VI. This is because ProsaBuddy shows much better performance than all the compared systems, so we infer that for the cases where ProsaBuddy failed, all the other compared system will also very likely fail, so we omit these experiments. The experiment results show that ProsaBuddy significantly outperforms the compared systems. Out of 2424 lemmas, PALM and Cobblestone only succeed 11 lemma, AutoRocq succeeds 22, RocqStar and OpenCode succeed 33, while ProsaBuddy succeed 1717. For the one lemma PALM and Cobblestone succeed, they use many fewer tokens. This is because of the way they work: they invoke the LLM for a specific number of times, and detailed error corrections rely on automated proof generation tools such as CoqHammer[21]. This differs from other agent-based systems, which conduct iterative dialogues with the LLM for both proof generation and error correction. Our benchmark targets lemmas that are not yet included in Prosa but are closely connected to the foundations provided by Prosa. Their proofs rely on existing Prosa definitions and basic lemmas. This selection is intentional: lemmas that are largely unrelated to the current Prosa foundation would require ProsaBuddy to invent new definitions and many intermediate lemmas from scratch, which is beyond its current capability. Accordingly, the experimental results should not be interpreted as showing that ProsaBuddy can prove real-time scheduling theorems in full generality. They instead evaluate whether ProsaBuddy can extend an existing mechanized library by proving new lemmas when the relevant definitions and many auxiliary results are already available. This reflects the positive feedback loop we aim to support: as Prosa grows to cover more real-time scheduling topics, ProsaBuddy can benefit from the richer foundation and help prove further lemmas. TABLE VI: Results of the Comparison Experiments and Ablation Study with our Built 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 ✘ ✘ ✘ ✘ ✘ ✘ ✘ - - ✘ - ✘ ✘ ✘ - - ✘ - ✘ 1 RocqStar ✘ ✘ - ✘ ✔ 23 ✘ ✘ ✘ ✘ ✘ ✘ ✘ - - ✘ - ✔ 587 ✘ ✔ 1,486 - - ✘ - ✘ 3 AutoRocq ✘ ✘ - ✘ ✔ 6 ✘ ✘ ✘ ✘ ✘ ✘ ✘ - - ✔ 1176 - ✘ ✘ ✘ - - ✘ - ✘ 2 Cobblestone ✘ ✘ - ✘ ✔ 2 ✘ ✘ ✘ ✘ ✘ ✘ ✘ - - ✘ - ✘ ✘ ✘ - - ✘ - ✘ 1 OpenCode ✘ ✘ - ✘ ✔ 247 ✘ ✘ ✘ ✔ 1,083 ✘ ✘ ✘ - - ✘ - ✔ 500 ✘ ✘ - - ✘ - ✘ 3 PB-w/o-S ✔ 25,410 ∞ ∞ - ✔ 23,440 ✔ 206 ✔ 3,760 ∞ ∞ ✔ 21,540 ✔ 535 ✘ ✔ 45,185 ∞ ∞ - - ✔ 4,084 - ✔ 601 ✔ 2,398 ✔ 896 - - ✔ 29,129 - ✘ 12 PB-w/o-D ✔ 23,056 ✔ 20,858 - ✔ 11,296 ✔ 186 ✔ 11,481 ✔ 2,617 ✘ ✔ 456 ∞ ∞ ✔ 30,334 ∞ ∞ - - ✔ 11,095 - ✔ 616 ✔ 8,798 ✔ 479 - - ✔ 8,680 - ✔ 29,137 14 PB-w/o-P ✔ 37,125 ✘ - ✘ ✔ 205 ✔ 30,139 ✔ 47,333 ✘ ✔ 6,511 ✔ 35,156 ✔ 24,619 ✘ - - ✔ 3,317 - ✔ 2,177 ✔ 9,354 ✔ 1,625 - - ✔ 27,604 - ✘ 12 PB-w/o-H ✔ 36,340 ∞ ∞ - ✔ 11,238 ✔ 358 ✔ 3,501 ✔ 1,257 ✔ 16,550 ✔ 1,398 ✔ 41,562 ✔ 31,716 ✘ - - ✔ 23,906 - ✔ 1,321 ✔ 5,096 ✔ 1,833 - - ✔ 21,157 - ✔ 9,278 15 ProsaBuddy ✔ 48,819 ✔ 42,027 ∞ ∞ ✔ 13,332 ✔ 281 ✔ 1,295 ✔ 2,077 ✔ 13,077 ✔ 1,888 ✔ 24,330 ✔ 36,004 ✔ 38,749 ✘ ✘ ✔ 6,736 ✘ ✔ 3,908 ✔ 2,229 ✔ 307 ✘ ∞ ∞ ✔ 31,614 ✘ ✔ 13,557 17 Note: The number under each ✔ represents the amount of token consumption to prove this lemma, which is in thousands of tokens. The results in Table VI report only a single run for each case by each system. Since LLM generation is inherently stochastic, repeating the evaluation multiple times per case would yield more robust conclusions. However, conducting such repeated runs for all cases would incur prohibitive time and costs. As a compromise, we select 66 cases to further conduct multi-run evaluations. These cases are selected based on the token consumption of ProsaBuddy in the above experiments, covering different difficult levels: #15 and #17 as the low-difficulty group, #8 and #22 as the medium-difficulty group, and #1 and #2 as the high-difficulty group. For each case, we run each system 55 times under the same configuration. x/5x/5 indicates that the system succeeds x times out of the five runs. For n=5n=5 runs with x successes, we compute pass@k=1−(n−xk)/(nk)pass@k=1- n-xk/ nk. Token counts are also reported in thousands. The numbers in the ‘Range’ and ‘Average’ rows represents the token consumption range and the average token consumption of the 55 runs. TABLE VII: Results of Five Runs 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 ProsaBuddy 5/5 5/5 5/5 4/5 4/5 4/5 pass@1 1 1 1 0.8 0.8 0.8 pass@3 1 1 1 1 1 1 Range 6,736–19,087 1,748-6,457 13,077–38,724 22,890–31,614 29,168–54,525 35,546–64,957 Average 11,471 3,669 25,220 28,120 44,171 50,630 The results in Table VII show that, across the 66 selected cases, ProsaBuddy achieves 2727 successful proofs out of 3030 total runs. It succeeds in all 55 runs on Cases #8, #15, and #17, and in 44 of 55 runs on Cases #1, #2, and #22. These repeated runs confirm that both proof outcomes and token consumption vary to some extent across individual executions. However, this variation does not alter the main comparative picture: ProsaBuddy attains at least four successes out of five runs on every selected case, whereas PALM yields no successful runs and OpenCode succeeds in only 22 of its 3030 runs. Furthermore, the estimated pass@3 for ProsaBuddy is 1.0 for all 66 cases. TABLE VIII: Results with Lemmas Selected from Prosa 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 - - - - - ProsaBuddy 10/10 10/10 8/10 9/10 9/10 6/10 1/5 Note: “# of tactics” represent the number of tactics used in its proof. We further conduct evaluations using more lemmas selected from Prosa. These lemmas are categorized into seven levels (L1–L7) based on proof length, measured by the number of tactics used in the proof. Each level contains 1010 lemmas, except L7: Prosa has 1212 L7 lemmas in total, among which we selected 55 as training lemmas and 55 as evaluation lemmas for this evaluation, with the evaluation lemmas strictly distinct from the training lemmas used in Section I-C. Unlike the our build benchmark, this experiment does not provide the agent with human-written proof hints. This is because many lemmas in Prosa are library-internal results and do not have corresponding human-written proofs in the literature. We observe that Prosa contains many families of similar proofs. For example, the same lemma is established under several related scheduling models, such as fixed-priority preemptive, non-preemptive, and limited-preemptive scheduling. Although these are technically different lemmas, their statements and proof structures can be very similar. In such cases, an agent with access to the full library may solve the target lemma largely by copying or lightly adapting an existing proof, rather than by generating the proof from the target statement and local context. This would make the evaluation less interesting. To solve this problem, for each lemma, we provide only the minimal Prosa slice required to compile the target file, computed from the transitive dependency closure of its required modules. In this way, the agent has enough formal context to prove the benchmark lemma, but it cannot search other parts of Prosa for the original proof or a similar proof. Similar to above experiments, we omit the experiments in L3-L7 for the compared systems, which are denoted by “–” in Table VIII. This is because, if a baseline shows poor ability to solve lemmas in lower-level groups, there is no reason to expect better performance on higher levels. As PALM, RocqStar, Autorocq, Cobblestone and OpenCode solved zero or only a very small number of lemmas at L2. Therefore, we did not further evaluate them on L3 and above. The experiment results with lemmas selected from Prosa confirm the superiority of ProsaBuddy. The results also show that ProsaBuddy still can successfully prove non-trivial lemmas even without human-written proof hints. TABLE IX: Experiment Results with Different Backbone LLMs 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 ∞ ∞ ✔ 13,332 ✔ 281 ✔ 1,295 ✔ 2,077 ✔ 13,077 ✔ 1,888 ✔ 24,330 ✔ 36,004 ✔ 38,749 ✘ ✘ ✔ 6,736 ✘ ✔ 3,908 ✔ 2,229 ✔ 307 ✘ ∞ ∞ ✔ 31,614 ✘ ✔ 13,557 17 DeepSeek-v4-flash ∞ ∞ ∞ ∞ - ∞ ∞ ✔ 959 ✔ 32,528 ✔ 7,406 ✘ ✔ 4,013 ∞ ∞ ∞ ∞ ∞ ∞ - - ✔ 6,205 - ✔ 2,262 ✔ 18,405 ✔ 5,624 - - ✔ 20,245 - ∞ ∞ 9 DeepSeek-v4-pro ∞ ∞ ∞ ∞ - ∞ ∞ ✔ 2,201 ∞ ∞ ✔ 8,749 ✘ ✔ 4,247 ✘ ✘ ✘ - - ✔ 20,898 - ✔ 768 ✘ ✔ 4,567 - - ✘ - ✘ 6 Gemini-3.1-flash-lite ✘ ∞ ∞ - ∞ ∞ ✔ 1,889 ∞ ∞ ∞ ∞ ∞ ∞ ✘ ∞ ∞ ✘ ✘ - - ∞ ∞ - ∞ ∞ ✘ ✔ 10,355 - - ✘ - ∞ ∞ 2 GPT-oss-120B ✘ ✘ - ✘ ✔ 1,192 ✘ ✘ ✘ ✘ ✘ ✘ ✘ - - ✘ - ✘ ✘ ✘ - - ✘ - ✘ 1 IV-B Ablation Study We conduct ablation experiments to evaluate the contribution of different components in ProsaBuddy, the result of which is also reported in Table VI. PB-w/o-S. This variant removes the proving skills from ProsaBuddy. It proves 1212 lemmas, fewer than the full ProsaBuddy does, demonstrating the effectiveness of the proving skills developed in Section I-C. PB-w/o-D. This variant removes the lemma decomposition mechanism and instead uses only the primary agent to prove a lemma. PB-w/o-D proves 1414 lemmas. The gap between PB-w/o-D and ProsaBuddy mainly appears on harder cases, i.e., lemmas on which ProsaBuddy spends more tokens. Token counts reveal a trade-off: ProsaBuddy sometimes spends more tokens because planning and delegation introduce extra interaction cost, but this overhead enables proofs that the single-agent variant cannot complete. PB-w/o-H. This variant removes the human-written proof hints from ProsaBuddy, i.e., it does not read the corresponding paper content. PB-w/o-H proves 1515 lemmas. The two cases where ProsaBuddy succeeds but PB-w/o-H does not are both relatively difficult lemmas. This suggests that for simple cases, the formal context in Prosa, including definitions, existing lemmas, and proof states, already provides substantial guidance for proof construction. However, for difficult lemmas, the human-written proof hints play a significant role. PB-w/o-P. This variant removes access to the full Prosa library and only provides the minimal dependent files needed to state the target lemmas. As a result, it can use basic definitions and low-level lemmas (related to the basic properties of the definitions) included in the dependent files, but cannot directly observe or reuse higher-level auxiliary lemmas in Prosa. PB-w/o-P proves 1212 lemmas. This shows that a full library context is important for extending an existing mechanized development. Without it, the agent needs to rediscover intermediate facts that are already available in Prosa, which signiciantly increase the difficulty to complete the proof. For most cases where PB-w/o-P succeeds, it consumes more token than ProsaBuddy, which witnesses such extra overhead even if the lemma is still proved. IV-C Different Backbone LLMs We further evaluate how the choice of different backbone LLM affects the performance of ProsaBuddy. The results are reported in Table IX. In these experiments, all components of ProsaBuddy are held constant except the backbone LLM. From the results we can see that the backbone LLM has a substantial impact on proof success: with the most powerful model, GPT-5.4, ProsaBuddy proves 17 lemmas, compared to 9 with DeepSeek-v4-flash, 6 with DeepSeek-v4-pro, 2 with Gemini-3.1-flash-lite, and 1 with GPT-oss-120B. Unexpectedly, DeepSeek-v4-flash outperforms DeepSeek-v4-pro. We currently do not have a clear explanation for this anomaly and will investigate its cause in future work. Overall, these results show that the agent framework, augmented external knowledge, and feedback from Rocq tools are not sufficient on their own; the reasoning capability of the backbone LLM is crucial for the performance of ProsaBuddy. We also observe that, on the subset of lemmas the weaker models can prove, they tend to consume more tokens on average than GPT-5.4, with a few exceptions. Similar to above, the mark “–” in Table IX denotes the omitted experiments to save time and cost, as for the difficult cases GPT-5.4 failed, the other weaker LLMs likely will also fail. V Discussions and Conclusions In this work, we present ProsaBuddy, an LLM-based agent system designed to lower the effort needed to develop mechanized real-time schedulability proofs. Evaluations show that ProsaBuddy can successfully prove many non-trivial lemmas. However, this is only a preliminary attempt in this direction; it has many limitations and ample room for further exploration. Although in this paper we introduce and evaluate ProsaBuddy as a standalone system that proves lemmas end-to-end, our ultimate goal is to build ProsaBuddy as a highly interactive tool. When a human expert intervenes in the proving process and provides guidance at points where ProsaBuddy gets stuck, ProsaBuddy becomes more effective and useful. We did not systematically evaluate ProsaBuddy with a human in the loop, because designing an objective and reproducible evaluation methodology for such interaction would be difficult. Nevertheless, we conducted some ad‑hoc interactive experiments. For example, for cases #13\#13 and #14\#14 in Table VI, which ProsaBuddy could not prove alone, a researcher with expertise in real‑time scheduling theory worked interactively with ProsaBuddy, injecting additional human instructions when ProsaBuddy was stuck or actively requested support. In this way, both lemmas were successfully proved in 22 hours and 33 hours, respectively. For comparison, a second researcher with a similar background independently proved them fully manually in Rocq, requiring 1414 hours and 1717 hours, respectively. A critical issue in automated theorem proving is the formalization of the lemmas themselves. This is especially important for schedulability lemmas, whose descriptions are lengthy and involve many definitions and hypotheses. Correct formalization is the foundation for the proof work: if a lemma is incorrectly formalized, its proof is meaningless. Therefore, the lemma must be formalized very carefully, a task that itself demands considerable effort. Assisting researchers during this formalization phase is thus also valuable. However, while lemma proving benefits from an automatic verifier (Rocq) that can check correctness, formalization lacks such a verifier. It is impossible to fully automate the checking of whether a formalization precisely captures the human’s intended meaning. Our future work will investigate how to utilize an LLM-based agent to assist the formalization of schedulability analysis lemmas. The decomposition guidelines and proving skills introduced in Section I are only a small subset of what can be added to improve the agent’s capabilities. We expect that ProsaBuddy users will develop their own skills to enhance the agent, and we look forward to an ecosystem in which users share their skills to collectively improve the system. Such an ecosystem would also create a feedback loop in which successful skills are refined, reused, and benchmarked across projects, accelerating collective improvement. On the other hand, these guidelines and skills are tailored to the capabilities of today’s LLMs. Given how rapidly LLMs are advancing, future LLMs may have much stronger reasoning abilities, rendering many previously useful skills obsolete. ProsaBuddy has the potential to be used more broadly. Proofreader [69] is an agentic system that helps researchers and authors find flaws in their own proofs. It actively seeks counterexamples and errors, without aiming to establish formal correctness. Given these complementary strengths, future work could explore how ProsaBuddy and other tools like Proofreader might jointly accelerate the discovery, refinement, and validation of new theorems. References [1] K. Bletsas, N. C. Audsley, W. Huang, J. Chen, and G. Nelissen (2018) Errata for three papers (2004-05) on fixed-priority scheduling with self-suspensions. Leibniz Transactions on Embedded Systems 5 (1), p. 02:1–02:20. Note: Art. no. 2 External Links: Document Cited by: §I. [2] M. Günzel and J. Chen (2020) Correspondence article: counterexample for suspension-aware schedulability analysis of EDF scheduling. Real-Time Systems 56 (4), p. 490–493. External Links: Document Cited by: §I. [3] J. Chen, G. Nelissen, W. Huang, M. Yang, B. Brandenburg, K. Bletsas, C. Liu, P. Richard, F. Ridouard, N. Audsley, R. Rajkumar, D. Niz, and G. Brüggen (2019) Many suspensions, many problems: a review of self-suspending tasks in real-time systems. Real-Time Systems 55 (1), p. 144–207. External Links: Document Cited by: §I. [4] K. Chen, M. Günzel, G. von der Brüggen, and J. Chen (2022) Critical instant for probabilistic timing guarantees: refuted and revisited. In IEEE Real-Time Systems Symposium (RTSS), External Links: Document Cited by: §I. [5] F. Cerqueira, F. Stutz, and B. B. Brandenburg (2016) PROSA: a case for readable mechanized schedulability analysis. In Euromicro Conference on Real-Time Systems (ECRTS), External Links: Document Cited by: §I, §I-B. [6] The coq proof assistant. Note: project web site, https://coq.inria.fr Cited by: §I. [7] S. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. Narasimhan, and Y. Cao (2023) ReAct: synergizing reasoning and acting in language models. In International Conference on Learning Representations (ICLR), Cited by: §I, §I-A. [8] Anomaly (2026) OpenCode: the open source coding agent. Note: SoftwareAccessed: September 8, 2026 External Links: Link Cited by: §I, §I-A. [9] The Rocq Development Team (2025) The rocq prover reference manual. Inria, CNRS, and contributors. Note: Version 9.2 External Links: Link Cited by: §I-A. [10] G. Gonthier, A. Mahboubi, and E. Tassi (2016) A Small Scale Reflection Extension for the Coq system. Research Report Technical Report R-6455, Inria Saclay Ile de France. Cited by: §I-B, §I-C. [11] F. Cerqueira, G. Nelissen, and B. B. Brandenburg (2018) On strong and weak sustainability, with an application to self-suspending real-time tasks. In Euromicro Conference on Real-Time Systems (ECRTS), Cited by: §I-B. [12] S. Bozhko and B. B. Brandenburg (2020) Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle. In Euromicro Conference on Real-Time Systems (ECRTS), External Links: ISBN 978-3-95977-152-8, ISSN 1868-8969, Document Cited by: §I-B. [13] K. Bedarkar, M. Vardishvili, S. Bozhko, M. Maida, and B. B. Brandenburg (2022) From intuition to Coq: a case study in verified response-time analysis of FIFO scheduling. In IEEE Real-Time Systems Symposium (RTSS), External Links: Document Cited by: §I-B. [14] P. Roux, S. Quinton, and M. Boyer (2022) A Formal Link Between Response Time Analysis and Network Calculus. In Euromicro Conference on Real-Time Systems (ECRTS), External Links: ISBN 978-3-95977-239-6, ISSN 1868-8969, Document Cited by: §I-B. [15] M. Maida, S. Bozhko, and B. Brandenburg (2022) Foundational response-time analysis as explainable evidence of timeliness. In Euromicro Conference on Real-Time Systems (ECRTS), Cited by: §I-B. [16] K. Bedarkar, L. Elbeheiry, M. Sammler, L. Gäher, B. Brandenburg, D. Dreyer, and D. Garg (2025) RefinedProsa: connecting response-time analysis with C verification for interrupt-free schedulers. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), External Links: Document Cited by: §I-B. [17] A. Mahboubi and E. Tassi (2022) Mathematical components. Zenodo. External Links: Document Cited by: §I-C. [18] M. Dénès, A. Mörtberg, and V. Siles (2012) A refinement-based approach to computational algebra in COQ. In International Conference on Interactive Theorem Proving (ITP), External Links: Document Cited by: §I-C. [19] B. Ekici, A. Mebsout, C. Tinelli, C. Keller, G. Katz, A. Reynolds, and C. Barrett (2017) SMTCoq: a plug-in for integrating smt solvers into coq. In International Conference on Computer Aided Verification (CAV), External Links: ISBN 978-3-319-63390-9 Cited by: §I-C. [20] B. Ekici, G. Katz, C. Keller, A. Mebsout, A. J. Reynolds, and C. Tinelli (2016) Extending SMTCoq, a Certified Checker for SMT (Extended Abstract). In International Workshop on Hammers for Type Theories (HaTT), Cited by: §I-C. [21] Ł. Czajka and C. Kaliszyk (2018) Hammer for Coq: automation for dependent type theory. Journal of Automated Reasoning 61 (1–4), p. 423–453. External Links: Document Cited by: §I-C, §IV-A. [22] D. Delahaye (2000) A Tactic Language for the System Coq. In International Conference on Logic for Programming and Automated Reasoning (LPAR), Cited by: §I-C. [23] B. Ziliani, D. Dreyer, N. R. Krishnaswami, A. Nanevski, and V. Vafeiadis (2015) Mtac: a monad for typed tactic programming in Coq. Journal of Functional Programming 25, p. 1–59. Note: Art. no. e12 External Links: Document Cited by: §I-C. [24] J. Kaiser, B. Ziliani, R. Krebbers, Y. Régis-Gianas, and D. Dreyer (2018) Mtac2: typed tactics for backward reasoning in Coq. In ACM SIGPLAN International Conference on Functional Programming (ICFP), External Links: Document Cited by: §I-C. [25] E. Tassi (2018) Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λ dialect). In International Workshop on Coq for Programming Languages (CoqPL), Cited by: §I-C. [26] M. Sozeau, S. Boulier, Y. Forster, N. Tabareau, and T. Winterhalter (2020) Coq Coq correct! verification of type checking and erasure for Coq, in Coq. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), External Links: Document Cited by: §I-C. [27] E. Komendantskaya, J. Heras, and G. Grov (2013) Machine learning in Proof General: interfacing interfaces. Electronic Proceedings in Theoretical Computer Science 118, p. 15–41. External Links: Document Cited by: §I-C. [28] K. Yang and J. Deng (2019) Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning (ICML), Cited by: §I-C. [29] L. Blaauwbroek, J. Urban, and H. Geuvers (2020) The tactician. In Conference on Intelligent Computer Mathematics (CICM), External Links: ISBN 978-3-030-53518-6 Cited by: §I-C. [30] A. Sanchez-Stern, Y. Alhessi, L. Saul, and S. Lerner (2020) Generating correctness proofs with neural networks. In ACM SIGPLAN International Workshop on Machine Learning and Programming Languages (MAPL), External Links: ISBN 9781450379960, Document Cited by: §I-C. [31] E. First, Y. Brun, and A. Guha (2020) TacTok: semantics-aware proof synthesis. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), External Links: Document Cited by: §I-C. [32] A. Kozyrev, G. Solovev, N. Khramov, and A. Podkopaev (2024) CoqPilot, a plugin for LLM-based generation of proofs. In IEEE/ACM International Conference on Automated Software Engineering (ASE), External Links: Document Cited by: §I-C, TABLE I, §IV-A. [33] M. Lu, B. Delaware, and T. Zhang (2024) Proof automation with large language models. In IEEE/ACM International Conference on Automated Software Engineering (ASE), External Links: ISBN 9798400712487, Document Cited by: §I-C, TABLE I, §IV-A. [34] A. Thakur, G. Tsoukalas, Y. Wen, J. Xin, and S. Chaudhuri (2024) An in-context learning agent for formal theorem-proving. In Conference on Language Modeling (COLM), Cited by: §I-C, TABLE I, §IV-A. [35] X. Liu, H. Liu, X. Yi, and J. Wang (2024) LLM-Enhanced Theorem Proving with Term Explanation and Tactic Parameter Repair. In Asia-Pacific Symposium on Internetware (Internetware), External Links: ISBN 979-8-4007-0705-6, Document Cited by: §I-C, TABLE I, §IV-A. [36] Y. Lu, H. Yang, X. Wang, G. Zhang, B. Li, C. Fu, C. Li, Y. Yuan, and A. C. Yao (2025) Clarifying before reasoning: a coq prover with structural context. Note: arXiv preprint arXiv:2507.02541 Cited by: §I-C, TABLE I, §IV-A. [37] K. Thompson, N. Saavedra, P. Carrott, K. Fisher, A. Sanchez-Stern, Y. Brun, J. F. Ferreira, S. Lerner, and E. First (2025) Rango: adaptive retrieval-augmented proving for automated software verification. In IEEE/ACM International Conference on Software Engineering (ICSE), External Links: ISBN 9798331505691, Document Cited by: §I-C, TABLE I, §IV-A. [38] M. Lu, Z. Zhou, D. Xie, S. Jia, B. Delaware, and T. Zhang (2025) Adaptive proof refinement with llm-guided strategy selection. Note: arXiv preprint arXiv:2510.25103 Cited by: §I-C, TABLE I, §IV-A. [39] A. Kozyrev, N. Khramov, G. Solovev, and A. Podkopaev (2026) RocqStar: leveraging similarity-driven retrieval and agentic systems for rocq generation. In International Conference on Autonomous Agents and Multiagent Systems (AAMAS), Cited by: §I-C, TABLE I, §IV-A. [40] S. R. Kasibatla, A. Agrawal, Y. Brun, S. Lerner, T. L. Ringer, and E. First (2026) Cobblestone: a divide-and-conquer approach for automating formal verification. In IEEE/ACM International Conference on Software Engineering (ICSE), External Links: Document Cited by: §I-C, TABLE I, §IV-A. [41] H. Tu, H. Zhao, Y. Song, M. Zafar, R. Meng, and A. Roychoudhury (2026) Agentic verification of software systems. In ACM International Conference on the Foundations of Software Engineering (FSE), External Links: Document Cited by: §I-C, TABLE I, §IV-A. [42] Y. Sun, C. Shi, H. Lyu, and Y. Xiong (2026) On reasoning-centric llm-based automated theorem proving. Note: arXiv preprint arXiv:2604.19558 Cited by: §I-C, TABLE I, §IV-A. [43] N. Zhang, N. Di, Z. Li, Y. Yao, and X. Ma (2026) Planning to hammer: difficulty-aware decomposition for automating rocq proofs. Note: arXiv preprint arXiv:2606.17981 Cited by: §I-C, TABLE I, §IV-A. [44] Y. Wu, A. Q. Jiang, W. Li, M. Rabe, C. Staats, M. Jamnik, and C. Szegedy (2022) Autoformalization with large language models. In Conference on Neural Information Processing Systems (NeurIPS), Cited by: §I-C. [45] A. Q. Jiang, S. Welleck, J. P. Zhou, W. Li, J. Liu, M. Jamnik, T. Lacroix, Y. Wu, and G. Lample (2023) Draft, Sketch, and Prove: Guiding formal theorem provers with informal proofs. In International Conference on Learning Representations (ICLR), Cited by: §I-C. [46] Q. Liu, X. Zheng, X. Lu, Q. Cao, and J. Yan (2025) Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach. In International Conference on Learning Representations (ICLR), Cited by: §I-C. [47] K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. J. Prenger, and A. Anandkumar (2023) LeanDojo: theorem proving with retrieval-augmented language models. In Conference on Neural Information Processing Systems (NeurIPS), Cited by: §I-C. [48] Z. Azerbayev, H. Schoelkopf, K. Paster, M. D. Santos, S. M. McAleer, A. Q. Jiang, J. Deng, S. Biderman, and S. Welleck (2024) Llemma: an open language model for mathematics. In International Conference on Learning Representations (ICLR), Cited by: §I-C. [49] H. Wang, H. Xin, C. Zheng, L. Li, Z. Liu, Q. Cao, Y. Huang, J. Xiong, H. Shi, E. Xie, J. Yin, Z. Li, H. Liao, and X. Liang (2024) LEGO-prover: neural theorem proving with growing libraries. In International Conference on Learning Representations (ICLR), Cited by: §I-C. [50] H. Xin, Z.Z. Ren, J. Song, Z. Shao, W. Zhao, H. Wang, B. Liu, L. Zhang, X. Lu, Q. Du, W. Gao, H. Zhang, Q. Zhu, D. Yang, Z. Gou, Z.F. Wu, F. Luo, and C. Ruan (2025) DeepSeek-prover-v1.5: harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. In International Conference on Learning Representations (ICLR), Cited by: §I-C. [51] H. Lin, Z. Sun, S. Welleck, and Y. Yang (2025) Lean-STar: learning to interleave thinking and proving. In International Conference on Learning Representations (ICLR), Cited by: §I-C. [52] P. Song, K. Yang, and A. Anandkumar (2025) Lean copilot: large language models as copilots for theorem proving in lean. In International Conference on Neuro-symbolic Systems (NeuS), Cited by: §I-C. [53] Y. Lin, S. Tang, B. Lyu, Z. Yang, J. Chung, H. Zhao, L. Jiang, Y. Geng, J. Ge, J. Sun, J. Wu, J. Gesi, X. Lu, D. Acuna, K. Yang, H. Lin, Y. Choi, D. Chen, S. Arora, and C. Jin (2026) Goedel-prover-v2: scaling formal theorem proving with scaffolded data synthesis and self-correction. In International Conference on Learning Representations (ICLR), Cited by: §I-C. [54] S. Varambally, T. Voice, Y. Sun, Z. Chen, R. Yu, and K. Ye (2026) Hilbert: recursively building formal proofs with informal reasoning. In International Conference on Learning Representations (ICLR), Cited by: §I-C. [55] A. Q. Jiang, W. Li, S. Tworkowski, K. Czechowski, T. Odrzygóźdź, P. Miłoś, Y. Wu, and M. Jamnik (2022) Thor: wielding hammers to integrate language models and automated theorem provers. In Conference on Neural Information Processing Systems (NeurIPS), Cited by: §I-C. [56] E. First, M. N. Rabe, T. Ringer, and Y. Brun (2023) Baldur: whole-proof generation and repair with large language models. In ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), Cited by: §I-C. [57] H. Wang, H. Xin, Z. Liu, W. Li, Y. Huang, J. Lu, Z. YANG, J. Tang, J. Yin, Z. Li, and X. Liang (2024) Proving theorems recursively. In Conference on Neural Information Processing Systems (NeurIPS), Cited by: §I-C. [58] K. Weng, L. Du, S. Li, W. Lu, H. Sun, H. Liu, and T. Zhang (2025) Autoformalization in the era of large language models: a survey. Note: arXiv preprint arXiv:2505.23486 Cited by: §I-C. [59] N. Giessing, H. Rahkooy, and M. Schubotz (2026) A survey on llms in automated theorem proving. Note: Zenodo preprint External Links: Document Cited by: §I-C. [60] The mathlib Community (2020) The Lean mathematical library. In ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), External Links: ISBN 9781450370974, Document Cited by: §I-A. [61] G. Tsoukalas, J. Lee, J. Jennings, J. Xin, M. Ding, M. Jennings, A. Thakur, and S. Chaudhuri (2024) PutnamBench: evaluating neural theorem-provers on the putnam mathematical competition. In Conference on Neural Information Processing Systems, Datasets and Benchmarks Track (NeurIPS), Cited by: §I-A. [62] The Rocq Development Team (2025) Vernacextend: rocq runtime api. Note: https://rocq-prover.org/doc/V9.1.0/api/rocq-runtime/Vernacextend/index.htmlRocq version 9.1.0, accessed September 15, 2026 Cited by: TABLE IV. [63] M. Bertogna, M. Cirinei, and G. Lipari (2005) Improved schedulability analysis of edf on multiprocessor platforms. In Euromicro Conference on Real-Time Systems (ECRTS), Cited by: §IV-A, TABLE V, TABLE V, TABLE V. [64] M. Bertogna and M. Cirinei (2007) Response-time analysis for globally scheduled symmetric multiprocessor platforms. In IEEE Real-Time Systems Symposium (RTSS), Cited by: §IV-A, TABLE V, TABLE V, TABLE V, TABLE V. [65] N. Guan, M. Stigge, W. Yi, and G. Yu (2009) New response time bounds for fixed priority multiprocessor scheduling. In IEEE Real-Time Systems Symposium (RTSS), Cited by: §IV-A, TABLE V, TABLE V, TABLE V, TABLE V, TABLE V, TABLE V, TABLE V, TABLE V, TABLE V, TABLE V, TABLE V. [66] Y. Sun, G. Lipari, N. Guan, and W. Yi (2014) Improving the response time analysis of global fixed-priority multiprocessor scheduling. In IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), Cited by: §IV-A, TABLE V, TABLE V, TABLE V. [67] S. Baruah, M. Bertogna, and G. Buttazzo (2015) Multiprocessor scheduling for real-time systems. Springer. Cited by: §IV-A, TABLE V, TABLE V. [68] A. Gujarati, F. Cerqueira, and B. B. Brandenburg (2013) Outstanding paper award: schedulability analysis of the linux push and pull scheduler with arbitrary processor affinities. In Euromicro Conference on Real-Time Systems (ECRTS), External Links: Document Cited by: §IV-A, TABLE V. [69] B. C. Ward (2026) Proofreader: informally auditing formal proofs with LLMs. Note: ManuscriptCollege of Connected Computing, Vanderbilt University External Links: Link Cited by: §V.