Paper deep dive

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

Sadat Shahriyar, Shareef Ahmed, Abdullah Al Arafat

Year: 2026Venue: arXiv preprintArea: cs.AIType: PreprintEmbeddings: 120

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 93%

Last extracted: 8/14/2026, 5:08:46 AM

Summary

The paper introduces PROVE-RT, an LLM-assisted framework for generating mechanized theorem prover scripts (PROSA/ROCQ) for schedulability analyses in real-time systems. It addresses the difficulty of manually constructing formal proofs by using dependency-aware informal sketches, retrieval from processed PROSA documentation, and staged skeleton generation. The authors created a corpus from 1,191 papers containing 13,134 informal sketches. Evaluation shows PROVE-RT achieves a 44.7% success rate, significantly outperforming direct LLM prompting.

Entities (6)

PROVE-RT · framework · 98%PROSA · software-library · 95%Rocq · theorem-prover · 95%LLMs · technology · 90%Real-Time Systems · domain · 90%Schedulability Analysis · concept · 90%

Relation Signals (5)

PROSA → builton → Rocq

confidence 95% · Prosa is a Rocq-based foundation for mechanized schedulability analysis

PROVE-RT → generates → PROSA/ROCQ scripts

confidence 95% · PROVE-RT... for generating PROSA/ROCQ scripts to mechanize schedulability analyses

PROVE-RT → uses → LLMs

confidence 95% · PROVE-RT is an LLM-assisted framework for generating PROSA/ROCQ scripts

PROVE-RT → achievessuccessrate → 44.7%

confidence 90% · PROVE-RT achieves a success rate of 44.7%

PROVE-RT → outperforms → direct prompting of LLMs

confidence 90% · 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%

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract: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.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

118,548 characters extracted from source content.

Expand or collapse full text

Prove-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs Sadat Shahriyar1, Shareef Ahmed2, Abdullah Al Arafat1 Affiliation: 1Florida International University, 2University of South Florida Email: sshahriy, aarafat@fiu.edu, shareefahmed@usf.edu Abstract 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,1911,191 real-time systems papers, containing 13,13413,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%44.7\%. These results show that retrieval-guided and staged LLM assistance can improve automated mechanization of schedulability analysis in Prosa/Rocq. I Introduction Safety-critical real-time systems (RTS) must undergo an offline certification process (typically in the form of a schedulability analysis) to ensure timing correctness at runtime. Traditionally, schedulability analyses have been devised through pen-and-paper proofs. Although this approach has enabled a rich body of real-time scheduling theory, it is increasingly difficult to sustain as systems become more complex. Moreover, manual proofs require careful validation, as subtle mistakes in intermediate lemmas or bounds can affect the final schedulability result and subsequent analyses that build upon it (e.g., [13, 8, 29, 10] are a few papers among many others that identify and address issues in earlier analyses). An alternative approach is to verify correctness through mechanized proofs. 9 developed the first mechanized theorem prover, Prosa, for real-time systems. Prosa provides a Rocq [38]-based foundation for mechanized schedulability analysis, offering a more rigorous approach for verifying the correctness of pen-and-paper proofs. Prosa is a repository of definitions and proofs for machine-checkable real-time scheduling theory, including task models, schedules, workload functions, interference notions, and schedulability results. By building on Rocq, Prosa enables schedulability analyses to be stated and checked with precision, thereby increasing confidence in the correctness of real-time systems theory. Unfortunately, mechanized verification does not eliminate the human effort required to construct formal proofs. This is evident from previous works. For example, CertiCAN, a Prosa-based Rocq tool for certifying CAN schedulability-analysis results, required 18,852 lines of Rocq code, excluding the Prosa proofs that it reused [18]. Similarly, integrating Prosa’s verified schedulability analysis into the RT-CertiKOS verified operating-system kernel required 4,135 lines of Rocq for the connection alone, including 1,900 lines for the translation interface to Prosa [20]. Beyond initial development costs, mechanized proofs also incur maintenance costs: for instance, 7 observed that even conceptually simple changes to the underlying model can invalidate existing mechanized proofs and require dozens of person-hours of proof maintenance. These examples suggest that although Prosa provides a reusable foundation for machine-checkable schedulability analysis, manual development and maintenance remain a substantial barrier to widespread adoption. To reduce the burden of script preparation for mechanized theorem provers [38, 30, 12, 40] in general cases, a growing body of work has explored automated theorem proving and proof automation using machine learning [5, 16, 6, 14, 34, 35, 11]. However, to the best of our knowledge, there has been no prior work on the automated mechanization of schedulability analyses for real-time systems. In this work, we introduce Prove-RT, a novel large-language-model (LLM)-assisted framework for generating mechanized Prosa proofs for schedulability analyses whose correctness can be verified mechanically. It is noteworthy that, beyond mechanizing existing schedulability analyses, Prove-RT may also facilitate the trustworthy use of generative AI for developing new schedulability analyses. As generative AI has shown promise across many scientific disciplines [43, 32, 36], Prove-RT can serve as a verification layer for validating AI-assisted or AI-generated schedulability results through mechanized checking. Challenges and Contributions. Although schedulability analyses are mathematically rigorous, they are typically expressed in a non-mechanized form that lacks the explicit structure required by theorem provers. Therefore, generating Prosa scripts for schedulability analyses differs fundamentally from conventional mathematical proof generation which is more widely studied in the literature. This introduces three key challenges: (i) limited mechanized RTS corpora, restricting LLM understanding of Prosa abstractions and proof patterns; (i) a formalization gap between structurally non-mechanized schedulability analyses and Prosa’s explicit proof structure; and (i) the complexity in the structure of schedulability lemmas/theorems compared to mathematical theorem-proving tasks. These challenges are elaborated in Section I. To overcome them, Prove-RT incrementally mechanizes schedulability analyses through staged formalization, dependency-aware proof construction, and retrieval-augmented grounding using RTS knowledge and Prosa documentation. In summary, this paper makes the following contributions: • We introduce Prove-RT, a framework for assisting the mechanization of schedulability analyses in Prosa/Rocq. To the best of our knowledge, Prove-RT is the first LLM-assisted framework targeting the Prosa-based mechanization of RTS analysis. • We develop a benchmark from 1,1911,191 real-time systems papers, comprising 13,13413,134 mechanization-oriented informal sketches and corresponding Prosa/Rocq script artifacts. The benchmark is intended to support future work on LLM-assisted theorem proving and formalization for real-time systems. • We analyze the key challenges, recurring failure modes, and corner cases encountered when generating Prosa/Rocq scripts with LLMs. This study provides practical insights for improving future automated mechanization tools for real-time systems analysis. Paper Organization. The remainder of the paper is organized as follows. Section I elaborates on the core challenges while mechanizing schedulability analysis with Prosa. Section I provides background on Prosa and reviews related work. Section IV introduces the notation used throughout the paper and formalizes the problem statement. Section V presents the design of Prove-RT. Section VII describes the construction of the system invariant dataset, the evaluation baselines and metrics, and the implementation details. Section VI provides an example on how the framework works. Section VIII presents the evaluation of Prove-RT. Finally, Section IX concludes the paper by discussing the limitations of Prove-RT and outlining directions for future work. I Challenges in Mechanizing Schedulability Analysis Automated theorem proving for real-time schedulability analysis introduces challenges that differ from the more commonly studied setting of LLM-based theorem proving for pure mathematics. In particular, the difficulty is not only to generate a proof script for a given theorem, but also to recover the formal structure needed to express schedulability analyses in Prosa/Rocq. A key limitation is the scarcity of mechanized training data for real-time schedulability analysis. Recent LLM-based theorem-proving systems benefit from large formal corpora [37, 46, 1, 44, 2, 41], which provide many examples of theorem statements, proof scripts, and reusable mathematical libraries. In contrast, public data for mechanized schedulability analysis is very limited. The Prosa library is the main available resource, but its scale is much smaller than mature mathematical proof libraries. This data scarcity limits the ability of LLMs to learn Prosa-specific abstractions, scheduling terminology, type-class assumptions, and proof patterns. Another challenge is the formalization gap between schedulability analyses as written in the real-time systems literature and the explicit proof structure required by Prosa. Schedulability analyses are usually presented through mathematical notation, prose explanations, assumptions, definitions, intermediate bounds, and proof sketches. Although these presentations are rigorous for human readers, they are not directly mechanizable. A Prosa/Rocq development must explicitly declare variables, hypotheses, type-class instances, section contexts, dependencies, and proof obligations. Therefore, an automated system must first identify the mechanization-relevant constructs, recover their dependencies, normalize notation, and map the extracted concepts to existing Prosa abstractions before proof generation can even begin. Schedulability-analysis lemmas are also structurally complex. They are often built on a hierarchy of task models, job parameters, arrival constraints, scheduling policies, workload definitions, interference bounds, and response-time properties. These definitions may depend on one another across multiple levels and are usually accompanied by many hypotheses. As a result, the complete formal context needed to state and prove a schedulability lemma in Prosa can span hundreds of lines. This creates a substantial burden on the LLM’s context handling and reasoning capabilities. Beyond the complexity of individual lemmas, Prosa is designed around reusable abstractions and lemmas that apply across different task models and scheduling policies. Whether an existing lemma can be used to prove a target result depends on whether its preconditions hold in the current proof context. Thus, proof generation requires more than selecting tactics: it requires constructing the right context, preserving dependency order, and ensuring that all required assumptions are available. These factors make automated mechanization of schedulability analysis substantially more difficult than direct proof generation for an already formalized theorem statement. I Preliminaries and Related Work In this section, we will discuss the necessary Prosa background and the related works on mechanized theorem provers and script generation. I-A Background on Prosa Prosa [9] is a Rocq library for mechanized schedulability analysis of RTS. It formalizes real-time scheduling concepts as Gallina (i.e., Rocq specification language) definitions and establishes schedulability results as machine-checked lemmas and theorems. Since Prosa is built in Rocq, a Prosa script follows the standard Rocq development model: required modules are imported, assumptions are introduced through sections and contexts, definitions are stated, and proof obligations are discharged using tactics. A key feature of Prosa developments is their reliance on explicit proof context. A Section groups together variables, hypotheses, and type-class constraints that are shared by the definitions and lemmas inside it. Prosa uses Rocq type classes to represent reusable modeling assumptions, such as task parameters, job parameters, scheduling policies, and system properties. Although these assumptions may be inferred automatically by Rocq via type-class resolution, the required instances must be available in the current context or imported environment for the script to type-check. Rocq follows a forward-referencing discipline: every definition, hypothesis, lemma, theorem, and imported module must be introduced before it is used. Thus, a valid Prosa development must be ordered so that all prerequisites of a proof are already available when the proof is checked. This makes dependency ordering and context construction central to writing correct Prosa scripts. We briefly summarize the Rocq/Prosa notions that are needed to follow the rest of the paper. • Proof script is the Rocq source code used to express a formal development. In Prosa, a proof script contains imports, definitions, assumptions, lemmas, theorems, and tactic-based proofs for schedulability analysis. • Proof environment refers to the collection of formal objects available during proof development. This includes imported libraries, previously defined concepts, declared assumptions, and already-proved lemmas or theorems. • Proof context refers to the local information available at a particular point in a proof. In Prosa, this often includes variables, hypotheses, task and job parameters, scheduling assumptions, and type-class instances introduced inside a section. • Proof goal is the proposition that remains to be proved. A schedulability theorem in Prosa may generate one or more proof goals involving task assumptions, workload bounds, interference bounds, or response-time guarantees. • Proof tactic is a command used to advance a proof by transforming the current goal into simpler subgoals or by solving it directly. Common Rocq tactics include intros, apply, rewrite, simpl, and lia. • Proof step is one application of a proof tactic. Each proof step changes the current proof state and moves the proof closer to completion. • Proof state is the complete status of an interactive proof at a given point, including the current goals and the local context. During proof construction, the proof state changes after each tactic is applied. • Type-class resolution is Rocq’s mechanism for automatically finding required instances of abstract interfaces. Prosa uses type classes to represent reusable modeling assumptions, such as job costs, task parameters, arrival information, and scheduling properties. • Proof obligation is a statement that must be proved before a development is complete. Lemmas, theorems, and corollaries introduce proof obligations, whereas definitions mainly introduce formal objects. • Compilation is the process of checking a Rocq/Prosa file. A file compiles only if all referenced objects are available, all statements are well typed, all type-class requirements are resolved, and all proof obligations are completed or explicitly admitted. A compilation error occurs when any of these conditions is violated, for example, due to missing imports, undefined variables, unresolved type-class instances, type mismatches, or incomplete proofs. Such errors indicate that the script is not yet a valid mechanized development. I-B Related Works Mechanized verification provides a rigorous way to validate mathematical and software artifacts by encoding definitions, assumptions, lemmas, and theorems in an interactive theorem prover (ITP), where each proof is checked by a small trusted kernel. Several ITPs, such as Rocq [38] (commonly known as Coq), Isabelle [30], Agda [40], and Lean [12], have been widely used in the verification community. These proof assistants have supported the verification of a broad range of software systems. For example, Rocq has been used to verify the CompCert C compiler [26], a lightweight relational database management system [28], and distributed systems through the Verdi framework [42]. Isabelle/HOL has been used to verify the seL4 operating-system kernel [24]. More recently, Lean has been used to formalize and verify neural networks through TorchLean [19]. In real-time systems, Prosa provides a Rocq-based foundation for mechanized schedulability analysis [9]. It formalizes core real-time scheduling concepts including task models, schedules, workload functions, interference notions, and schedulability results. Building on this foundation, prior work has used Prosa to mechanize and validate several schedulability-analysis results including response-time analysis, CAN schedulability certification, FIFO scheduling, busy-window reasoning, and connections between response-time analysis and network calculus [7, 18, 4, 27, 33]. These works demonstrate the value of mechanized verification for increasing confidence in real-time systems theory. However, they still require substantial manual proof engineering and domain expertise. To reduce the burden of manual proof development, prior approaches have proposed various methods for generating proof tactics, selecting relevant premises, and guiding proof search using learned models [5, 16, 6, 14, 34, 35, 11]. More recently, large language models (LLMs) have shown promise in generating formal proofs and assisting interactive theorem proving [21, 23, 45, 22, 31, 39]. However, these efforts have largely focused on general-purpose theorem proving or domains such as mathematics and software verification. To the best of our knowledge, there has been no prior effort to automatically generate Prosa proofs for mechanized schedulability analysis from real-time systems papers. IV Framework Model and Problem Statement IV-A Framework Model We first define the main objects used throughout the Prove-RT pipeline. Schedulability Analysis (A). Let A be a schedulability analysis for an RTS scheduling problem. Such an analysis is typically presented using mathematical definitions, assumptions, lemmas, theorems, corollaries, and proof arguments. Unlike standard Rocq tactic-generation tasks, A is not given as a proof goal inside an existing proof environment. Instead, it is a schedulability test whose formal constructs, dependency structure, and proof obligations must be recovered before mechanization. System Invariant (I). We use the term system invariant to refer to any mechanization-relevant construct in A that must be represented in the final Prosa/Rocq development. A system invariant may be a definition, hypothesis, assumption, lemma, theorem, corollary, fix-point, or other formal claim required to establish the correctness of the schedulability test. We denote the set of extracted system invariants by I=i1,i2,…,in.I=\i_1,i_2,…,i_n\. Informal Sketch (Kj\K_j\). An informal sketch KjK_j describes the statement of the invariant iji_j, the intuition behind it, and the intended proof outline. These sketches serve as the intermediate representation between the natural-language schedulability analysis and the generated Prosa/Rocq script. Each invariant ij∈Ii_j∈ I is associated with an informal sketch KjK_j. Dependency Structure (GDG_D). The extracted invariants form a dependency structure. We represent this structure as a directed acyclic graph (DAG) GD=(I,D),G_D=(I,D), where each node corresponds to a system invariant and each directed edge represents a dependency, e.g., an edge (ip,ij)∈D(i_p,i_j)∈ D means that invariant iji_j depends on ipi_p. Thus, ipi_p must appear earlier than iji_j in the generated Prosa/Rocq script. The DAG, therefore, defines the order in which invariants should be formalized. This ordering is required because Rocq is forward-referencing: all definitions, assumptions, lemmas, theorems, and imports must be introduced before they are used. Prosa Documentation Corpus (P). Let P be the processed Prosa documentation corpus. P contains documentation fragments, definitions, assumptions, reusable lemmas, and example proof structures extracted from the Prosa library. For each invariant iji_j, the retrieval module selects a relevant subset Rj⊆PR_j P to provide the library-specific context needed for script generation. The generated script is built incrementally according to the dependency order induced by GDG_D. IV-B Problem Statement Given a schedulability analysis A and a processed Prosa documentation corpus P, the goal of Prove-RT is to generate a dependency-ordered Prosa/Rocq script S that mechanizes the schedulability analysis and compiles under the Prosa/Rocq environment as: M:(A,P)→S,M:(A,P)→ S, where M denotes the Prove-RT generation pipeline and S=s1,s2,…,snS=\s_1,s_2,…,s_n\ is the generated Prosa/Rocq script. Each code block sj∈Ss_j∈ S is intended to formalize the corresponding system invariant ij∈Ii_j∈ I. A successful output must satisfy three requirements. First, each generated code block sjs_j must correctly represent the corresponding extracted invariant iji_j. Second, the ordering of code blocks in S must respect the dependency graph GD=(I,D)G_D=(I,D), so that every prerequisite invariant is introduced before any invariant that depends on it. Third, the final script S must compile under the Prosa/Rocq environment. We decompose this objective into two subproblems. Skeleton Generation (via MskelM_skel). The first subproblem is skeleton generation. For each invariant iji_j, the skeleton-generation module uses the informal sketch KjK_j, the retrieved Prosa context RjR_j, the dependency graph GDG_D, and the partial Prosa/Rocq script already generated for earlier invariants, denoted by S<jS_<j, to produce a structurally valid Prosa/Rocq code block: Mskel:(Kj,Rj,GD,S<j)→sj.M_skel:(K_j,R_j,G_D,S_<j)→ s_j. After the skeleton-generation stage, some generated Prosa/Rocq fragments contain proof-bearing constructs, such as lemmas, theorems, or corollaries, whose proof bodies were intentionally left as Admitted. We refer to these unfinished proof bodies as deferred proof obligations. The proof-completion stage attempts to replace each Admitted. placeholder with a valid Rocq proof. For each deferred proof associated with sjs_j, the proof-completion module takes the current partial script S<jS_<j, the corresponding informal sketch KjK_j, and the retrieved Prosa context as input RjR_j, and generates a proof fragment πj _j intended to replace the Admitted. placeholder. Proof Completion (via MproofM_proof). The second subproblem is proof completion. For each deferred proof in sjs_j, the proof-completion module uses the current partial script S<jS_<j, the informal sketch KjK_j, and the retrieved Prosa context RjR_j to generate a proof fragment πj _j: Mproof:(S<j,sj,Kj,Rj)→πj.M_proof:(S_<j,s_j,K_j,R_j)→ _j. The generated proof fragment πj _j is intended to replace the corresponding Admitted placeholder. It is accepted only if the resulting Prosa/Rocq script is checked successfully by the Rocq compiler. If compilation fails, compiler feedback or proof-state information is used to guide repair. Thus, the problem addressed by Prove-RT is broader than next-tactic prediction. It requires transforming a real-time systems schedulability analysis into a dependency-ordered Prosa/Rocq script that can be mechanically checked by the proof assistant. V Prove-RT Framework Prove-RT consists of five stages: (1) Extracting system invariants, informal sketches, and dependency graph from formally written schedulability analysis; (2) Processing the Prosa documentation into retrieval-ready fragments; (3) retrieving relevant documentation and examples, with dependency recovery for proof-oriented modules; (4) generating and validating a structurally correct proof skeleton with deferred obligations; and (5) completing the deferred proofs using iterative repair. We explain these stages in the following subsections. Fig. 1 illustrates an overview of the Prove-RT. Fig. 1: Overview of the proposed Prosa/Rocq proof-generation pipeline. V-A System Invariant Extraction Extraction of Invariants and Sketches. The first stage of Prove-RT transforms the input, schedulability analysis A, into the intermediate representation required for mechanization, consisting of a set of system invariants I, their corresponding informal sketches Kj\K_j\, and a dependency graph GD=(I,D)G_D=(I,D). This stage is necessary as schedulability analyses in the RTS literature are usually written for mathematical presentation rather than direct mechanization. As a result, the constructs needed for Prosa/Rocq generation may appear in different forms, including prose explanations, equations, definitions, lemmas, theorems, claims, or corollaries. To facilitate this process, Prove-RT first prompts an LLM to identify candidate system invariants from schedulability test A. The LLM is guided using carefully designed prompts that include practical examples and detailed guardrails to ensure consistency and accuracy in the output. For each extracted invariant ij∈Ii_j∈ I, the LLM generates an informal sketch KjK_j. Informal sketches provide a structured, step-by-step description of each system invariant in plain text, capturing both the logical flow and the intended proof outline. An example informal sketch is outlined in Listing 4 in Appendix -A1. Construction of Dependency Graph. The extracted dependency information is used to construct the dependency graph GD=(I,D)G_D=(I,D). For each invariant iji_j, the LLM identifies other invariants that must be established before iji_j can be formalized. Each such relation is represented as an edge in D. The extracted invariants are then ordered according to this graph so that, when the Prosa/Rocq script is generated, prerequisites are introduced before the constructs that depend on them. The resulting unit-level informal sketches, ordered by GDG_D, form the primary input to the subsequent stages of Prove-RT. V-B Prosa Documentation Processing The second stage of Prove-RT constructs the processed Prosa documentation corpus P used for retrieval. This stage is necessary because direct LLM-based generation of Prosa/Rocq scripts is difficult without library-specific context. The Prosa library relies on domain-specific abstractions, type-class assumptions, reusable lemmas, and proof conventions that are often not available to a pretrained model. Thus, the Prosa documentation is processed into retrieval-ready fragments so that later stages can retrieve relevant proof constructs for each invariant iji_j. The Prosa documentation is organized into six main modules: Analysis, Behavior, Implementation, Model, Results, and Util. These modules are used to guide the construction of P. In particular, the Results module is used primarily as a source of complete proof examples, since it contains formally verified schedulability results. The remaining modules provide supporting context, including system definitions, modeling assumptions, formal definitions, reusable lemmas, and auxiliary proof components. As the modules differ in both structure and purpose, they are processed using two chunking strategies. Proof-Oriented Chunking. For the Analysis and Results modules, proof-oriented chunks are used which pairs each formal code block with its corresponding descriptive text. This preserves the connection between a proof component and the explanation that motivates it, allowing retrieval to operate over meaningful proof-level units such as definitions, lemmas, and theorems. During retrieval, the retrieved proof-level units are augmented with their relevant dependencies, so that lemmas, theorems, and definitions are provided together with the supporting constructs required for script generation. This dependency reconstruction step is described in the next section V-C. Section-Level Chunking. For the remaining modules, section-level chunks are used, since these modules are typically organized around smaller and more self-contained concepts, assumptions, or helper components. The resulting set of documentation fragments forms the processed corpus P. During retrieval, Prove-RT selects a relevant subset Rj⊆PR_j P for each invariant iji_j, which provides the LLM with Prosa-specific context for generating the corresponding Prosa/Rocq code block sjs_j. V-C Retrieval Process Query Construction. The retrieval stage constructs the context Rj⊆PR_j P for each invariant iji_j. Given the informal sketch KjK_j, the goal is to retrieve the most relevant fragments from the processed Prosa documentation corpus P so that the skeleton-generation module has access to library-specific definitions, assumptions, lemmas, and example proof structures. Each informal sketch may contain information about multiple invariants, including a target invariant and the prerequisites on which it depends. To preserve the dependency order induced by GDG_D, we process the sketches one invariant at a time. For each invariant iji_j, its corresponding sketch KjK_j is used as the retrieval unit. For each informal sketch unit KjK_j, three components are used as retrieval queries: the statement of the invariant, the intuition underlying it, and the conclusion it establishes. Together, these components capture both the formal objective and the supporting reasoning of the target proof step. Retrieval is performed independently for the statement, intuition, and conclusion queries, producing a ranked top-k list for each component. The retrieved candidates are then merged, and the highest-scoring documentation sections are selected as the retrieval context RjR_j. Dependency Recovery for Proof-Oriented Modules. For candidates retrieved from the Analysis or Results modules, an additional syntax-aware dependency recovery step is applied before adding them to RjR_j. These modules contain proof-oriented files in which later sections often rely on earlier definitions, hypotheses, lemmas, or typeclass contexts. Since Rocq follows a forward-referencing discipline, a section with index N can depend only on preceding sections with indices from 00 to N−1N-1 within the same file. Prove-RT exploits this ordering to recover the earlier sections needed to make the retrieved proof fragment usable in downstream generation. The dependency recovery step assigns different weights to occurrences of identifiers based on their syntactic context. Identifiers before the Proof. keyword are treated as the strongest signals because they appear in the type-level statement of the declaration. Explicit references following tactics such as apply and rewrite are treated as medium-strength signals, while other proof-level tokens receive lower weight because they are more likely to include tactic noise or external-library names. If an identifier appears in multiple contexts, its maximum weight is kept to preserve the strongest dependency signal without double counting. After extracting candidate identifiers from the three zones, each identifier is assigned a weight w(x)=max(α⋅[x∈ZA],β⋅[x∈ZB],γ⋅[x∈ZC]),w(x)= (α·F[x∈ Z_A],\;β·F[x∈ Z_B],\;γ·F[x∈ Z_C] ), Here, ZAZ_A, ZBZ_B, and ZCZ_C denote the sets of identifiers extracted from the type-level zone, the explicit-reference zone, and the remaining proof-token zone, respectively. The parameters α, β, and γ are weighting coefficients assigned to these zones, with α>β>γα>β>γ to reflect the relative strength of the dependency signal provided by each syntactic context. To improve robustness, tokens are filtered out that are unlikely to correspond to meaningful local dependencies, such as grammar keywords, logical connectives, single-character tokens, self-references, and proof-local names introduced during tactics. After extracting identifiers, they are matched against declarations in earlier sections of the same file. A section receives a score when it defines a matched identifier, weighted by the identifier’s dependency score; sections with nonzero scores are treated as likely direct dependencies. Unmatched identifiers contribute a small score to the imports file to prevent external-library references from being ignored. Because direct dependencies may themselves depend on earlier constructs, the procedure is applied recursively and arranges the recovered sections in their original order so that each construct appears before it is used. The recovered dependencies are assembled with the retrieved section before being included in RjR_j. Imports are placed at the top level, code fragments are ordered for compilation, and unicode operators are normalized when needed. A lean version is first compiled containing only the recovered dependencies to reduce context size and noise. If this fails, a full-context version is used that includes all predecessor sections from the same file, which helps capture implicit dependencies such as typeclass requirements. For the remaining modules, the documentation is more naturally organized into self-contained sections. Therefore, each section is treated as a single retrieval unit, the top-k matching sections are retrieved, and used directly without additional dependency recovery. V-D Skeleton Code Generation The skeleton-generation stage addresses the first subproblem defined in Section IV. For each invariant iji_j, it generates a structurally valid Prosa/Rocq code block sjs_j using the invariant’s informal sketch KjK_j, the retrieved context RjR_j, the dependency graph GDG_D, and the partial script S<jS_<j generated for earlier invariants. This stage deliberately separates structure generation from proof generation. Generating the correct type signature of a Prosa/Rocq construct, including its name, variable bindings, typeclass constraints, and statement, is generally more tractable for a language model than simultaneously discovering a valid proof strategy. Therefore, the skeleton stage focuses on producing well-typed declarations and statements, while proof bodies are deferred to the proof-completion stage. This decomposition provides an intermediate artifact that can be checked by coqc, allowing Prove-RT to detect structural errors before attempting proof synthesis. Prompt Construction. For each invariant iji_j, we construct the skeleton-generation prompt from four inputs: the informal sketch KjK_j, the retrieved Prosa context RjR_j, the dependency graph GDG_D, and the partial script S<jS_<j. These components provide the model with the relevant library context, examples of Prosa structure, and the current proof context. The informal sketch KjK_j for the target section is appended last so that it remains the immediate generation objective. In addition to this contextual information, the prompt includes two generation rules to ensure that the generated block sjs_j is structurally meaningful. First, proof-skeleton rule is enforced where every proof-bearing construct must be generated with a deferred proof obligation using Admitted., and no proof tactics are allowed at this stage. Thus, the model may generate either of the following forms: Lemma foo : <statement>. Proof. Admitted. or Lemma foo : <statement>. Admitted. Non-proof-bearing constructs, such as definitions, declarations, and type-level specifications, must instead be generated in full because they do not create deferred proof obligations and are required for the skeleton to type-check. Second, assumption-integrity rules are enforced. In preliminary experiments, a common failure mode was that the model made the proof artificially easy by turning claims that should be proven into unsupported assumptions. To prevent this, the prompt explicitly prohibits introducing unsupported hypotheses, restating the target claim as an assumption, or encoding the proof obligation in a vacuous way. Claims from KjK_j must remain proof-bearing constructs, while genuine preconditions must be encoded as part of the corresponding formal statement. These rules make skeleton checking more reliable. If the generated block sjs_j fails to compile, the error is more likely to indicate a structural problem, such as an incorrect type, undefined identifier, or missing import, rather than a failed or misleading proof attempt. They also prevent the model from producing speculative proof bodies that may appear syntactically valid but are semantically incorrect and difficult to repair later. Fig. 2: Skeleton code generation Validation and Retry. After each generation attempt, the produced skeleton sjs_j is validated in two steps. First, it is checked that all proof-bearing constructs follow the admitted-only rule and contain no completed or partial proof bodies. Second, sjs_j is appended to the current partial script S<jS_<j and the resulting script is compiled with coqc. This verifies structural validity and type correctness. Non-proof-bearing constructs are accepted directly because they do not open a Proof. block. If validation or compilation fails, the section is regenerated; sections that repeatedly fail are logged and skipped so that the pipeline can continue. V-E Skeleton Code Completion After skeleton generation, each code block sjs_j may contain proof-bearing constructs whose proof bodies are deferred using Admitted. The goal of the completion stage is to generate a proof fragment πj _j that replaces each deferred proof and makes the resulting Prosa/Rocq script compile. For each deferred proof, the completion module uses the current partial script S<jS_<j, the corresponding informal sketch KjK_j, and the retrieved Prosa context RjR_j as input. In this way, the system builds directly on the previous stage: the skeleton provides the formal statement and context, while the completion stage focuses only on filling in the missing proofs. Batch Completion with Iterative Repair. Prove-RT prompts LLM to generate the full proof body for a deferred proof in one response. The generated proof fragment πj _j replaces the corresponding Admitted. placeholder in sjs_j, and the resulting partial script is then checked with the Rocq compiler. Furthermore, to ensure that the generated script proves the intended target lemma rather than circumventing it, we include a proof-integrity checker. The checker validates the LLM-generated proof and detects whether the model has modified the original problem, introduced unsupported auxiliary facts, or shifted the main proof obligation into a separate construct. Edits outside the intended proof region are treated as invalid. Concretely, the checker flags constructs such as Axiom, Parameter, Parameters, Conjecture, Conjectures, Admitted, admit, and Abort. It also detects whether the LLM introduces new global lemmas or definitions outside the proof region that effectively carry the main proof burden. Such modifications are rejected because they may allow the script to compile without actually proving the original lemma. At the same time, the checker permits harmless changes that do not alter the meaning of the theorem, such as importing additional trusted libraries from Prosa or MathComp etc. If the script compiles successfully and the proof-integrity checker reports no violations, the script is accepted. If compilation fails or any violation is reported by the proof-integrity checker, Prove-RT enters an iterative repair loop in which compiler feedback guides corrections. At each iteration, the error message and its location are extracted from the compiler output and incorporated into a repair prompt together with the informal sketch KjK_j and the retrieved context RjR_j. The LLM then proposes a revised proof fragment, which is inserted into the section and checked again. This process is attractive because it allows the model to generate an entire proof in one step, while still benefiting from compiler-guided repair when the initial attempt is incorrect. Fig. 3: Batch Completion with Iterative Repair VI Illustrative Example We illustrate the end-to-end workflow of Prove-RT using a concrete schedulability analysis drawn from the RTS literature, starting with the extraction of intermediate representations and leading to the final machine-verified Prosa script. VI-A Source Material and Extraction We consider the paper “Worst-Case Timing Requirements of Real-Time Tasks with Time Redundancy” [25] as a representative example. From this paper, we extract the following definition and claim, which characterize the worst-case timing requirements of a task under fault-tolerant execution. The formal notations introduced in the paper are as follows: Worst-Case Timing Requirement: Let ai(ki)a_i(k_i) denote the additional processing time and runtime overhead required to tolerate kik_i faults during the mission time of a task T~i T_i. The worst-case timing requirement Wi(ki)W_i(k_i) of T~i T_i is given by Wi(ki)=Wi(0)+Ai(ki),W_i(k_i)=W_i(0)+A_i(k_i), (1) where Ai(ki)A_i(k_i) denotes the worst-case value of ai(ki)a_i(k_i) and Wi(0)W_i(0) represents the failure-free worst-case execution time (WCET). Retry-Based Redundancy: Assume that a task restarts from the beginning after each fault, with no rollback recovery. Let R∗R^* denote the constant restart overhead. Then the worst-case timing requirement under the retry mechanism is Wi(ki)=ki⋅(R∗+Wi(0))+Wi(0).W_i(k_i)=k_i·(R^*+W_i(0))+W_i(0). (2) These results are automatically extracted and structured using LLM. The extraction process identifies the formal statement, variables, assumptions, and conclusions associated with each invariant. In addition, it also produced an informal sketch. We provide the complete JSON extraction and the corresponding informal sketch in Appendix -A1. A notable property of the extraction is that it is dependency-aware. For each invariant, we identify the previously introduced invariants on which it depends; this information is recorded explicitly in the extracted representation. These dependencies induce a partial order that governs the subsequent formalization pipeline: an invariant is formalized only after all of its dependencies have been processed. In this example, Claim 1 depends on Definition 1, so the definition must first be formalized. Since Prosa follows an interpreted execution model in Rocq, all prerequisite definitions and constructs must be available before they are referenced, making dependency-aware ordering essential for correct compilation. VI-B Retrieval-Augmented Generation Given the informal sketch of an invariant, the next step is to translate it into a Prosa script. To support this translation, we employ retrieval-augmented generation (RAG) over the Prosa codebase. We use the statement, conclusion, and intuition fields from the informal sketch as query, retrieve their independent results and keep the top-k results from two complementary sources: (i) example scripts that demonstrate similar constructs or proof patterns, and (i) documentation fragments describing the syntax, semantics, and usage conventions of relevant Prosa modules. Together, these provide the LLM with sufficient context to generate correct and idiomatic Prosa script. VI-C Skeleton Code Generation Using the retrieved context, we prompt the LLM to generate skeleton code—a structurally complete, type-checkable Prosa script in which all imports, section boundaries, type-class contexts, variable declarations, and definition bodies are fully specified, while every proof obligation is replaced by Admitted. Listing 1 shows the skeleton code generated for the motivating example. Listing 1: Skeleton code generated from the informal sketch. All structural elements are fully elaborated; the proof body is deferred via Admitted. ⬇ Require Export prosa.util.all. Require Export prosa.behavior.time. Require Export prosa.model.task.concept. Require Export prosa.model.aggregate.workload. Section WorstCaseTimingRequirement. Context Task : TaskType. Context ‘TaskCost Task. Context Job : JobType. Context ‘JobTask Job Task. Context ‘JobCost Job. Variable W_i_0 : work. Variable k_i : nat. Variable R_star : work. Definition W_i_k_i (A_i_k_i : work) : work := W_i_0 + A_i_k_i. Lemma W_i_k_i_retry : W_i_k_i (k_i * (R_star + W_i_0)) = k_i * (R_star + W_i_0) + W_i_0. Proof. Admitted. End WorstCaseTimingRequirement. The skeleton faithfully encodes the structure of both invariants. Definition 1 is realized as the function W_i_k_i, which takes the fault-tolerance overhead A_i_k_i as an argument and returns its sum with the failure-free WCET W_i_0. The Prosa type work, defined as nat, represents discrete units of processor service. Claim 1 is stated as Lemma W_i_k_i_retry, which asserts that instantiating W_i_k_i with the retry-specific overhead yields exactly Equation (2). The type-class contexts (TaskType, JobType, TaskCost, etc.) anchor the formalization within Prosa’s modeling framework and ensure that the definitions are compatible with the library’s broader infrastructure. The Admitted. directive instructs Rocq to accept the lemma statement without proof, allowing the entire file to type-check successfully. This confirms that the formalization structure—imports, scoping, type-class resolution, and the lemma statement itself—is sound before any proof synthesis is attempted. VI-D Proof Completion In the final phase, we prompt the LLM a second time to discharge the Admitted obligations. This two-phase decomposition is deliberate: by supplying the complete skeleton as context, the LLM gains visibility into the surrounding definitions, type-class instances, and any auxiliary lemmas, enabling it to generate proof tactics that are consistent with the broader formalization. The prompt includes the retrieved context from the RAG step, the full skeleton code, and an instruction to complete a specific Admitted block. For this example, the LLM produces the following proof: Listing 2: Completed proof of the retry-based worst-case timing requirement ⬇ Lemma W_i_k_i_retry : W_i_k_i (k_i * (R_star + W_i_0)) = k_i * (R_star + W_i_0) + W_i_0. Proof. unfold W_i_k_i. lia. Qed. The proof proceeds in two steps. First, unfold W_i_k_i δ-reduces the definition, exposing the underlying goal: W_i_0+ki×(R∗+W_i_0)=ki×(R∗+W_i_0)+W_i_0. W\_i\_0+k_i×(R^*+ W\_i\_0)=k_i×(R^*+ W\_i\_0)+ W\_i\_0. This is an equality over natural numbers that follows directly from the commutativity of addition. The lia tactic, which implements a decision procedure for linear integer arithmetic, discharges it automatically. The completed script compiles under Rocq and confirms that the retry-based worst-case timing requirement is a valid instantiation of the general fault-tolerant WCET model formalized in Prosa. This example demonstrates how our pipeline systematically transforms informal real-time scheduling results into machine-verified Prosa proofs through a structured sequence of extraction, retrieval-augmented skeleton generation, and targeted proof completion. A second illustrative example can also be found in Appendix -F. VII Experimental Setup We evaluate Prove-RT by investigating the following research questions (RQs). RQ1: To what extent can Prove-RT formalize schedulability tests as Prosa/Rocq scripts? RQ2: How does the dependency depth of informal sketches influence the success of mechanization? RQ3: How does the choice of retrieval method affect the effectiveness of Prove-RT? VII-A System Invariant Dataset Construction As one of the main artifacts of this work, Prove-RT System Invariant Dataset is constructed, which is a large-scale collection of schedulability-analysis invariants designed to support and evaluate LLM-assisted Prosa/Rocq mechanization. The dataset provides instances of the framework objects introduced earlier: schedulability analyses A, extracted invariant sets I, informal sketches KjK_j, and dependency graphs GD=(I,D)G_D=(I,D). Figure 4 presents a high-level overview of the system invariant corpus collection process. To construct the source corpus for system-invariant extraction, schedulability-analysis papers were collected from established real-time systems and embedded systems venues. The IEEE Xplore API was used to retrieve paper metadata. The search was restricted to major venues, including RTSS, RTAS, ECRTS, EMSOFT, RTCSA, RTNS, RSS, and IROS. The full search query and venue list are provided in Appendix -B. The API returned 1,991 paper records. For each record, the metadata was extracted to locate the corresponding full-text PDF. Since the IEEE Xplore API does not directly support bulk full-text PDF downloads, a semi-automated browser-assisted workflow was used with personal access credentials. For each paper, the PDF URL was extracted from the retrieved metadata and was opened in an authenticated browser session using Selenium. Then Selenium was used to interact with the Chrome PDF viewer and trigger the download action automatically. Because authenticated sessions may expire during long download runs, the workflow also included a session-recovery mechanism that restored access through automated browser interactions. After retrieval, duplicate files caused by overlapping searches or repeated download sessions were removed, resulting in approximately 1,870 unique papers. Each collected PDF was then converted into a structured XML representation using GROBID. The XML format preserves document structure, making it more suitable for LLM-based extraction than raw PDF text. This structured representation was used as input to the invariant extraction stage of Prove-RT. In our implementation, we used Gemini-2.5-Flash as the LLM and prompted it to identify candidate system invariants I from each schedulability analysis and to extract their summaries, informal sketches KjK_j, and dependency information for constructing GDG_D. The prompts included examples and guardrails to encourage consistent output and to distinguish mechanization-relevant constructs from general explanatory text. After Gemini extraction, a deterministic validation pass was applied to filter structurally invalid outputs before constructing the final dataset. The validator constructed an inter-invariant dependency graph from the extracted identifier and dependencies fields, where each invariant is represented as a node, and each resolved dependency is represented as a directed edge from the dependent invariant to its prerequisite. To resolve dependency references, the validator uses a three-stage matching process: exact, normalized, and fuzzy matching. Exact matching requires the dependency string to match an extracted identifier character-for-character. Normalized matching canonicalizes both dependency strings and candidate identifiers by lowercasing text, replacing formatting artifacts such as backticks and underscores with spaces, removing non-alphanumeric punctuation, and collapsing repeated whitespace. If both exact and normalized matching fail, fuzzy matching compares the normalized dependency string against all normalized candidate identifiers using a character-level similarity score and links it only to the highest-scoring candidate when the score exceeds 0.880.88. This step is intended to recover near-duplicate identifiers with minor residual formatting differences while avoiding spurious dependency edges. Using the resolved dependency graph, the validator checks for unresolved dependencies, self-dependencies, forward references, and dependency cycles. Papers are labeled as keep, review, or reject: papers with dependency cycles or an unresolved-dependency ratio above 0.150.15 are rejected, papers with weaker structural issues are marked for review, and structurally valid papers are retained. After this filtering step, the retained corpus contained 1,1911,191 papers and 13,13413,134 informal sketches. Another important characteristic of the retained system invariant dataset is the distribution of extracted constructs by type. As discussed earlier, each unit-level informal sketch contains a target invariant together with the dependencies required to establish it. Consequently, a single sketch may include multiple system invariants that must be introduced and proved sequentially before the final target invariant can be mechanized. We therefore analyze the full set of system invariants appearing across all collected sketches. This analysis reveals substantial variation in how authors formulate and name system invariants. Across the collected papers, 73 distinct raw invariant types were identified. To make these invariants compatible with Rocq-based proof development, they were normalized into six broader categories corresponding to supported proof constructs: definitions, hypotheses, lemmas, theorems, corollaries, and fixpoints. The complete fine-grained mapping from raw sketch kinds to Rocq keywords is provided in Appendix -H. Overall, the extraction process produced 13,134 normalized system invariants, including their dependency information. Table I reports the distribution of invariants across the normalized categories. Fig. 4: System Invariant Dataset Collection We further analyze the number of invariants appearing in each unit-level informal sketch. Each sketch contains a target invariant together with the dependencies that must be established before the target can be mechanized. The resulting corpus is both an input to Prove-RT and a reusable artifact for studying LLM-assisted mechanization of real-time systems schedulability analyses. The distribution is described in Appendix -G. VII-B Baselines Prove-RT is compared against direct LLM-based generation of Prosa/Rocq scripts. Since recent LLMs have shown strong capability in proof synthesis and Rocq code generation, and since Prosa is built on top of Rocq, these baselines evaluate whether LLMs can mechanize real-time systems schedulability analyses without the additional guidance introduced by PROVE-RT. We consider two baseline settings. First, the LLM is prompted to mechanize a target invariant using only the corresponding text from the original schedulability-analysis paper, without external Prosa documentation or skeleton-code generation. Second, the LLM is provided with the extracted informal sketch for the target invariant, but receives no retrieval support and does not use the skeleton-code generation stage. These baselines measure how far direct LLM generation can go without dependency-aware retrieval, skeleton generation, and proof-repair mechanisms. VII-C Evaluation Metrics Prove-RT counts a generated script as successful only if it is accepted by the Rocq proof checker; that is, the completed proof must compile without errors, contain no remaining deferred proof obligations, and pass the proof-integrity checker without any reported violations. This follows the standard proof-assistant acceptance criterion used in prior Rocq proof-generation work, where generated proofs are considered correct only when they lead the theorem prover to proof termination with Qed [11, 39]. To measure the effectiveness of Prove-RT, we use success rate, a standard metric used in prior work to evaluate Rocq code and proof generation [44, 17, 15]. Success rate is measured as the fraction of proof constructs for which the tool generates a successful proof script: Success Rate=NSNT,Success Rate= N_SN_T, (3) where NSN_S denotes the number of successfully mechanized sketches with successful proof scripts, and NTN_T denotes the total number of evaluated sketches. VII-D Implementation Details For the system invariant extraction stage, Gemini-2.5-Flash was employed as the backbone large language model. The model is prompted with structured, guardrailed instructions alongside few-shot examples to ensure consistent XML parsing. For the retrieval-augmented generation (RAG) component, the retrieval corpus was constructed from the CoqDoc-generated HTML documentation of Prosa, yielding 5,0975,097 documentation fragments from 356356 source files. Three retrieval strategies were evaluated: BM25, dense retrieval, and hybrid retrieval. For dense retrieval, the nomic-embed-code-7b was used to generate vector embeddings and store them in a FAISS vector index. For each query, the top-K most relevant documentation chunks were selected, with K=5K=5, and they were provided as context to the LLM during skeleton generation. The proof completion pipeline uses Claude-Opus-4.6. It is executed in two phases. In the first phase, the skeleton code is synthesized with Admitted. directives to verify type-checking and type-class resolution. In the second phase, the LLM is prompted to discharge individual proof obligations using automation tactics for linear integer arithmetic. All interaction with the interactive theorem prover is managed via an automated script running Rocq version 9.1.0. TABLE I: Distribution of extracted elements by category Category Invariant Count Percentage # Raw Kinds Definition 6817 51.9% 17 Lemma 4144 31.6% 38 Theorem 1822 13.9% 1 Corollary 228 1.7% 1 Fixpoint 115 0.9% 14 Hypothesis 8 0.1% 2 TOTAL 13134 100.0% 73 The dataset construction and semi-automated PDF collection workflows are executed via Selenium driving an authenticated Chrome browser session. Text extraction and document structuring are processed using GROBID to convert raw PDFs into structured XML. The entire pipeline is implemented in Python 3.10 and evaluated on an Ubuntu 24.04 LTS server equipped with an Intel Xeon w5-3423 processor with 12 cores and 24 hardware threads, and 64GB of system RAM. VIII Evaluation We evaluate Prove-RT according to the three research questions introduced in Section VII. Evaluation of RQ1. To evaluate the effectiveness of Prove-RT, we compare it against direct Prosa/Rocq script generation using state-of-the-art LLMs, including GPT and Claude. Although these models have demonstrated strong general capabilities in generating Rocq code, their ability to generate Prosa scripts for mechanizing schedulability analyses remains unclear. We therefore conduct a pilot study to assess how well these models perform in this domain-specific setting. We then evaluate how Prove-RT guides these models for producing mechanically checkable Prosa/Rocq scripts. For this evaluation, we performed a human-in-the-loop curation step to select a representative subset from the retained invariant corpus. The selection focused on scheduling-analysis categories that are well aligned with existing Prosa abstractions while still spanning different levels of mechanization difficulty. These categories include uniprocessor fixed-priority response-time analysis, uniprocessor EDF response-time or demand-bound analysis, FIFO/FCFS response-time analysis, non-preemptive and limited-preemptive analyses, blocking and resource-sharing analyses, self-suspending task analyses, multiprocessor global EDF/global fixed-priority analysis, and multiprocessor partitioned scheduling analysis. After curation, the final evaluation corpus contained 109109 papers and 1,9041,904 unit-level informal sketches. From this curated evaluation corpus, we further selected a smaller evaluation subset of 300300 unit-level informal sketches using proportional stratified sampling over dependency-depth categories. Let ncn_c denote the number of sketches in category c, and let N denote the total number of sketches in the curated corpus. For each category, we computed the sampling quota as qc=300⋅ncN.q_c=300· n_cN. We first selected ⌊qc⌋ q_c sketches from each category and then assigned the remaining slots to the categories with the largest fractional remainders. Within each category, sketches were sampled uniformly at random using a fixed seed of 4242 for reproducibility. TABLE I: Overall mechanization success across generation modes. Mode Formalized Success Rate Paper Statements + GPT-5 0/300 0.0% Informal Sketch + GPT-5 0/300 0.0% Informal Sketch + Claude-Opus-4.6 1/300 0.33% PROVE-RT-hybrid 123/300 41.0% PROVE-RT-bm25 126/300 42.0% PROVE-RT-dense 134/300 44.7% Prove-RT achieves the best performance among the evaluated approaches when used with dense RAG, mechanizing 134134 informal sketches and achieving a success rate of 44.7%44.7\%. This result is encouraging because automated formalization remains challenging even in more established proof-assistant settings; prior neural theorem-proving systems such as Rango and GPass report success rates of approximately 32%32\% and 35%35\%, respectively [39, 11]. Although these results are not directly comparable due to differences in benchmarks and proof domains, they provide useful context for interpreting the difficulty of the task. Given that Prove-RT operates in the specialized and low-resource setting of Prosa-based real-time systems mechanization, a 44.7%44.7\% success rate indicates substantial progress. Other retrieval methods also perform competitively within Prove-RT: BM25 mechanizes 126126 sketches with a success rate of 42.0%42.0\%, while hybrid retrieval mechanizes 123123 sketches with a success rate of 41.0%41.0\%. In contrast, direct generation with GPT fails to mechanize any construct, whether prompted with paper statements or informal sketches. Claude mechanizes only 11 sketch from the informal sketches, corresponding to a success rate of 0.33%0.33\%. These results suggest that direct prompting, even with structured informal sketches, is insufficient for reliable Prosa/Rocq generation. The detailed comparison is shown in Table I. An interesting observation from the direct-generation baselines is that both GPT and Claude often produce compilable Rocq scripts without actually using Prosa. In these cases, the generated scripts may type-check in Rocq, but they do not rely on the definitions, abstractions, or verified results provided by the Prosa library. Since our goal is to mechanize real-time systems schedulability analyses within Prosa, we count such outputs as failures. In our study, Claude produced compilable scripts for 3939 of the 300300 informal sketches. However, only 11 of these scripts used Prosa; the remaining 3838 were generic compilable Rocq scripts and were therefore discarded. The behavior was even more pronounced for GPT, it generated 148148 compilable Rocq scripts out of 300300 attempts, but none of them used Prosa. These results further highlight the limitation of direct LLM prompting, even when the generated output is syntactically valid and type-correct in Rocq, it may fail to mechanize the target schedulability analysis in the intended Prosa framework. This confirms that decomposing the task into sketch-guided retrieval, skeleton generation, and proof completion improves the reliability of LLM-assisted Prosa mechanization. Observation I. Prove-RT is substantially more effective than direct LLM prompting for Prosa/Rocq mechanization. On the 300300 sampled informal sketches, Prove-RT-dense achieves the best result, mechanizing 134134 sketches with a success rate of 44.7%44.7\%. By contrast, direct generation with GPT-5 produces no valid Prosa mechanizations, and Claude-Opus-4.6 succeeds on only 11 sketch (0.33%0.33\%). This demonstrates that successful mechanization requires more than general Rocq generation ability; it requires Prosa-aware retrieval, dependency-aware structuring, and staged proof generation. (a) BM25 (b) Hybrid (c) Dense Fig. 5: Mechanization success by dependency depth for different retrieval methods. For readability, the plot shows sketches with at most 1010 sections. For each dependency depth, the blue bar shows the total number of sketches and the orange bar shows the number successfully formalized by Prove-RT. Evaluation of RQ2. To evaluate how the structural complexity of an informal sketch affects mechanization, we group the 300300 sampled informal sketches by the number of sections they contain. In our dataset, each sketch is decomposed into a sequence of sections, where later sections may depend on definitions, assumptions, or intermediate results introduced earlier in the sketch. Thus, the number of sections serves as a proxy for the dependency depth and mechanization complexity of the sketch. For each group, we compare the total number of sketches against the number of sketches that Prove-RT successfully formalizes as compilable Prosa/Rocq scripts. Figure 5 shows the distribution of total and successfully formalized sketches across different section counts. Each pair of bars corresponds to sketches with the same number of sections: the first bar shows the total number of sketches in that group, while the second bar shows how many of them were successfully mechanized by Prove-RT. The trend suggests that section count is a useful indicator of mechanization difficulty. Sketches with fewer sections typically correspond to simpler formalization tasks, such as isolated definitions or short proof obligations, where the generated Prosa/Rocq code depends on limited prior context. In contrast, sketches with many sections require Prove-RT to preserve a longer chain of definitions, assumptions, and intermediate results. This increases the likelihood that an error in an earlier generated code block propagates to later blocks and causes the final script to fail compilation. Consequently, failures in high-section-count sketches often reflect compound challenges, such as missing or incorrect prerequisites, mismatched identifiers, or insufficient retrieved context. At the same time, successful cases among multi-section sketches show that Prove-RT can mechanize nontrivial dependency structures rather than only isolated constructs or single-step proof obligations. It is important to note that the number of sections is only an approximate measure of complexity. Some short sketches may contain difficult proof obligations, while some longer sketches may consist mostly of definitions or straightforward intermediate claims. Nevertheless, section count provides a useful aggregate view of how dependency depth affects end-to-end mechanization success. Observation I. The success of Prove-RT decreases as sketches contain more sections, suggesting that deeper dependency chains make mechanization harder. Nevertheless, Prove-RT succeeds on several multi-section sketches, indicating that its dependency-aware extraction, retrieval, and staged generation strategy can support nontrivial schedulability-analysis mechanization. Evaluation of RQ3. Prior work such as [39] uses BM25-style sparse retrieval to retrieve relevant proof context. Sparse retrieval is a natural baseline because it is effective when the query and target documents share exact identifiers, theorem names, library symbols, or domain-specific terminology. However, the retrieval setting in Prove-RT is different. The Prosa documentation contains both formal code blocks and descriptive text explaining the logical role of definitions, lemmas, assumptions, and proof patterns. Moreover, for each code block, we generate an additional LLM-based description so that the retrieval corpus captures not only the surface syntax of the code but also its intended semantic role. This motivates our evaluation of different retrieval methods. In Prove-RT, retrieval queries are derived from the informal sketch KjK_j, which describes the statement, intuition, and conclusion of a target invariant in natural language. These queries often do not share exact tokens with the corresponding Prosa documentation or code identifiers, even when they refer to the same concept. Dense retrieval is therefore useful because it maps both sketch-derived queries and documentation descriptions into a shared semantic embedding space. At the same time, sparse retrieval may still be useful for recovering exact Prosa identifiers, theorem names, and library-specific terminology. TABLE I: Effect of retrieval method on Prove-RT. Retrieval All Sections Proven Sections Compiled Hybrid 123/300 (41.0%) 608/1393 (43.6%) BM25 126/300 (42.0%) 559/1393 (40.1%) Dense 134/300 (44.7%) 597/1393 (42.9%) Table I compares retrieval methods using two complementary metrics. The first metric, All Sections Proven, measures end-to-end mechanization success: a sketch is counted as successful only when all of its sections are formalized and compiled in dependency order. The second metric, Sections Compiled, measures local section-level success across all generated sections. Dense retrieval achieves the best end-to-end mechanization performance, proving all sections for 134134 out of 300300 sketches (44.7%44.7\%). BM25 and Hybrid also perform competitively, proving 126126 and 123123 sketches, respectively. At the section level, however, Hybrid compiles the largest number of individual sections, with 608608 compiled sections out of 13931393 (43.6%43.6\%), slightly higher than Dense with 597/1393597/1393 (42.9%42.9\%). This shows that local section-level compilation does not always translate into full-sketch mechanization, since a sketch is counted as fully mechanized only if all of its sections compile together in dependency order. TABLE IV: Retrieval performance by target construct kind. Kind Hybrid BM25 Dense Definition 112/278 (40.3%) 114/278 (41.0%) 125/278 (45.0%) Lemma 8/19 (42.1%) 9/19 (47.4%) 8/19 (42.1%) Theorem 3/3 (100.0%) 3/3 (100.0%) 1/3 (33.3%) Table IV further breaks down performance by target construct kind. Dense retrieval performs best on definition sketches, proving 125125 out of 278278 cases (45.0%45.0\%), suggesting that semantic retrieval is effective for matching informal descriptions to Prosa definitions. However, for proof-bearing constructs, the trend is different. Combining lemmas and theorems, BM25 proves 1212 out of 2222 proof-bearing sketches (54.5%54.5\%), Hybrid proves 1111 out of 2222 (50.0%50.0\%), and Dense proves 99 out of 2222 (40.9%40.9\%). This suggests that sparse and hybrid retrieval are particularly useful when proof completion depends on exact lemma names, theorem identifiers, or library-specific proof patterns. Thus, while dense retrieval gives the strongest end-to-end performance overall, lexical retrieval remains important for proof-bearing constructs where exact Prosa references are often needed. Overall, dense retrieval is most effective for semantic alignment, whereas sparse and hybrid retrieval remain valuable for proof-bearing constructs that depend on exact Prosa references. Observation I. The choice of retrieval method affects both section-level compilation and end-to-end mechanization. Dense retrieval achieves the best overall result, fully mechanizing 134/300134/300 sketches (44.7%44.7\%), while Hybrid compiles the most individual sections, with 608/1393608/1393 compiled sections (43.6%43.6\%). This suggests that semantic retrieval is especially useful for completing full dependency chains, while sparse retrieval remains useful for exact identifier and lemma-name matches. IX Conclusion This paper introduced Prove-RT, an LLM-assisted framework for generating mechanized Prosa/Rocq scripts for schedulability analyses in real-time systems literature. Prove-RT combines dependency-aware informal sketch extraction, retrieval from processed Prosa documentation, staged skeleton generation, and proof completion to guide LLMs toward Prosa-aware mechanization. Our evaluation shows that direct prompting of state-of-the-art LLMs is insufficient for reliable Prosa generation, while Prove-RT achieves a success rate of 44.7%44.7\% with dense retrieval. We also construct a mechanization-oriented corpus of informal sketches with dependency information. The corpus can facilitate future research on LLM-assisted mechanization of schedulability analyses, as domain-specific datasets for Prosa/Rocq-based schedulability analysis are currently lacking and remain a major bottleneck for automated script generation. As a research prototype, Prove-RT still faces challenges with deeper dependency chains and proof-bearing constructs that require precise Prosa context. Future work will improve retrieval, incorporate richer proof-state feedback, and extend the framework to broader classes of schedulability analyses. Moreover, we will study the capabilities of LLMs to generate schedulability constraints for new scheduling problems, for which Prove-RT can be used to mechanically verify the correctness of LLM-generated schedulability results. References [1] Z. Azerbayev, B. Piotrowski, H. Schoelkopf, E. W. Ayers, D. Radev, and J. Avigad (2023) ProofNet: autoformalizing and formally proving undergraduate-level mathematics. External Links: 2302.12433, Link Cited by: §I. [2] K. Bansal, S. Loos, M. Rabe, C. Szegedy, and S. J. Wilcox (2019) HOList: an environment for machine learning of higher order logic theorem proving. In Thirty-sixth International Conference on Machine Learning (ICML), External Links: Link Cited by: §I. [3] S.K. Baruah, A.K. Mok, and L.E. Rosier (1990) Preemptively scheduling hard-real-time sporadic tasks on one processor. In [1990] Proceedings 11th Real-Time Systems Symposium, Vol. , p. 182–190. External Links: Document Cited by: §-F, §-F1. [4] 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 1 of fifo scheduling. In 2022 IEEE Real-Time Systems Symposium (RTSS), Vol. , p. 197–210. External Links: Document Cited by: §I-B. [5] L. Blaauwbroek, M. Olšák, J. Rute, F. I. Schaposnik Massolo, J. Piepenbrock, and V. Pestun (2024) Graph2Tac: online representation learning of formal math concepts. In Proceedings of the 41st International Conference on Machine Learning, Proceedings of Machine Learning Research, Vol. 235, p. 4046–4076. External Links: Link Cited by: §I, §I-B. [6] L. Blaauwbroek, J. Urban, and H. Geuvers (2020) The tactician: a seamless, interactive tactic learner and prover for coq. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings, Berlin, Heidelberg, p. 271–277. External Links: ISBN 978-3-030-53517-9, Link, Document Cited by: §I, §I-B. [7] S. Bozhko and B. B. Brandenburg (2020) Abstract response-time analysis: a formal foundation for the busy-window principle (artifact). Dagstuhl Artifacts Ser. 6, p. 03:1–03:2. External Links: Link Cited by: §I, §I-B. [8] R. J. Bril, J. J. Lukkien, R. I. Davis, and A. Burns (2006) Message response time analysis for ideal controller area network (can) refuted. External Links: Link Cited by: §I. [9] F. Cerqueira, F. Stutz, and B. B. Brandenburg (2016) PROSA: a case for readable mechanized schedulability analysis. In 2016 28th Euromicro Conference on Real-Time Systems (ECRTS), Vol. , p. 273–284. External Links: Document Cited by: §I, §I-A, §I-B. [10] 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 Syst. 55 (1), p. 144–207. External Links: ISSN 0922-6443, Link, Document Cited by: §I. [11] Y. Chen, Z. Sun, G. Wang, and D. Hao (2025) Gpass: a goal-adaptive neural theorem prover based on coq for automated formal verification. In Proceedings of the IEEE/ACM 47th International Conference on Software Engineering, ICSE ’25, p. 29–41. External Links: ISBN 9798331505691, Link, Document Cited by: §I, §I-B, §VII-C, §VIII. [12] L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer (2015) The lean theorem prover (system description). In Automated Deduction - CADE-25, A. P. Felty and A. Middeldorp (Eds.), Cham, p. 378–388. Cited by: §I, §I-B. [13] R. Devillers and J. Goossens (2000) Liu and layland’s schedulability test revisited. Inf. Process. Lett. 73 (5–6), p. 157–161. External Links: ISSN 0020-0190, Link, Document Cited by: §I. [14] E. First, Y. Brun, and A. Guha (2020) TacTok: semantics-aware proof synthesis. 4 (OOPSLA). External Links: Link, Document Cited by: §I, §I-B. [15] E. First, Y. Brun, and A. Guha (2020) TacTok: semantics-aware proof synthesis. 4 (OOPSLA). External Links: Link, Document Cited by: §VII-C. [16] E. First and Y. Brun (2022) Diversity-driven automated formal verification. In Proceedings of the 44th International Conference on Software Engineering, ICSE ’22, New York, NY, USA, p. 749–761. External Links: ISBN 9781450392211, Link, Document Cited by: §I, §I-B. [17] E. First and Y. Brun (2022) Diversity-driven automated formal verification. In Proceedings of the 44th International Conference on Software Engineering, ICSE ’22, New York, NY, USA, p. 749–761. External Links: ISBN 9781450392211, Link, Document Cited by: §VII-C. [18] P. Fradet, X. Guo, and S. Quinton (2023) CertiCAN certifying can analyses and their results. Real-Time Syst. 59 (2), p. 160–198. External Links: ISSN 0922-6443, Link, Document Cited by: §I, §I-B. [19] R. J. George, J. Cruden, X. Zhong, H. Zhang, and A. Anandkumar (2026) TorchLean: formalizing neural networks in lean. External Links: 2602.22631, Link Cited by: §I-B. [20] X. Guo, M. Lesourd, M. Liu, L. Rieg, and Z. Shao (2019) Integrating formal schedulability analysis into a verified os kernel. In Computer Aided Verification, I. Dillig and S. Tasiran (Eds.), Cham, p. 496–514. External Links: ISBN 978-3-030-25543-5 Cited by: §I. [21] J. M. Han, J. Rute, Y. Wu, E. Ayers, and S. Polu (2022) Proof artifact co-training for theorem proving with language models. In International Conference on Learning Representations, External Links: Link Cited by: §I-B. [22] A. Q. Jiang, W. Li, J. M. Han, and Y. Wu (2021) LISA: language models of ISAbelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving (AITP), Aussois, France, p. 17:1–17:3. External Links: Link Cited by: §I-B. [23] 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 Advances in Neural Information Processing Systems, Vol. 35, p. 8360–8373. External Links: Link Cited by: §I-B. [24] G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood (2009) SeL4: formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP ’09, New York, NY, USA, p. 207–220. External Links: ISBN 9781605587523, Link, Document Cited by: §I-B. [25] H. Lee, H. Shin, and S. Min (1999) Worst case timing requirement of real-time tasks with time redundancy. In Proceedings Sixth International Conference on Real-Time Computing Systems and Applications. RTCSA’99 (Cat. No.PR00306), Vol. , p. 410–414. External Links: Document Cited by: §VI-A. [26] X. Leroy (2009) Formal verification of a realistic compiler. Commun. ACM 52 (7), p. 107–115. External Links: ISSN 0001-0782, Link, Document Cited by: §I-B. [27] M. Maida, S. Bozhko, and B. B. Brandenburg (2022) Foundational Response-Time Analysis as Explainable Evidence of Timeliness (Artifact). Dagstuhl Artifacts Series 8 (1), p. 7:1–7:2. Note: Keywords: hard real-time systems, response-time analysis, uniprocessor, Coq, Prosa, fixed priority, EDF, preemptive, non-preemptive, verification External Links: ISSN 2509-8195, Link, Document Cited by: §I-B. [28] G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky (2010) Toward a verified relational database management system. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’10, New York, NY, USA, p. 237–248. External Links: ISBN 9781605584799, Link, Document Cited by: §I-B. [29] G. Nelissen, J. Fonseca, G. Raravi, and V. Nélis (2015) Timing analysis of fixed priority self-suspending sporadic tasks. In 2015 27th Euromicro Conference on Real-Time Systems, Vol. , p. 80–89. External Links: Document Cited by: §I. [30] T. Nipkow, M. Wenzel, and L. C. Paulson (2002) Isabelle/hol: a proof assistant for higher-order logic. Springer-Verlag, Berlin, Heidelberg. External Links: ISBN 3540433767 Cited by: §I, §I-B. [31] S. Polu and I. Sutskever (2020) Generative language modeling for automated theorem proving. ArXiv abs/2009.03393. External Links: Link Cited by: §I-B. [32] Z. Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yang, Z. F. Wu, Z. Gou, S. Ma, H. Tang, Y. Liu, W. Gao, D. Guo, and C. Ruan (2025) DeepSeek-prover-v2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. External Links: 2504.21801, Link Cited by: §I. [33] P. Roux, S. Quinton, and M. Boyer (2022) A Formal Link Between Response Time Analysis and Network Calculus (Artifact). Dagstuhl Artifacts Series 8 (1), p. 3:1–3:3. Note: Keywords: Response Time Analysis, Network Calculus, dense time, discrete time, response time, formal proof, Coq External Links: ISSN 2509-8195, Link, Document Cited by: §I-B. [34] A. Sanchez-Stern, Y. Alhessi, L. Saul, and S. Lerner (2020) Generating correctness proofs with neural networks. In Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, MAPL 2020, New York, NY, USA, p. 1–10. External Links: ISBN 9781450379960, Link, Document Cited by: §I, §I-B. [35] A. Sanchez-Stern, E. First, T. Zhou, Z. Kaufman, Y. Brun, and T. Ringer (2023) Passport: improving automated formal verification using identifiers. ACM Trans. Program. Lang. Syst. 45 (2). External Links: ISSN 0164-0925, Link, Document Cited by: §I, §I-B. [36] Z. Shen, N. Huang, F. Yang, Y. Wang, G. Gao, T. Xu, J. Jiang, W. He, P. Yang, M. Sun, H. Ju, P. Wu, B. Dai, and B. Dong (2025) REAL-prover: retrieval augmented lean prover for mathematical reasoning. External Links: 2505.20613, Link Cited by: §I. [37] (2019) The lean mathematical library. CoRR abs/1910.09336. External Links: Link, 1910.09336 Cited by: §I. [38] (2026) The rocq prover. Note: Available at https://rocq-prover.org/doc/V9.2.0/refman/index.html. Last accessed: 2026-05-21 Cited by: §I, §I, §I-B. [39] 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 Proceedings of the IEEE/ACM 47th International Conference on Software Engineering, ICSE ’25, p. 347–359. External Links: ISBN 9798331505691, Link, Document Cited by: §I-B, §VII-C, §VIII, §VIII. [40] (2007) Towards a practical programming language based on dependent type theory. External Links: Link Cited by: §I, §I-B. [41] 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. External Links: 2407.11214, Link Cited by: §I. [42] J. R. Wilcox, D. Woos, P. Panchekha, Z. Tatlock, X. Wang, M. D. Ernst, and T. Anderson (2015) Verdi: a framework for implementing and formally verifying distributed systems. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’15, New York, NY, USA, p. 357–368. External Links: ISBN 9781450334686, Link, Document Cited by: §I-B. [43] R. Xin, C. Xi, J. Yang, F. Chen, H. Wu, X. Xiao, Y. Sun, S. Zheng, and K. Shen (2025) BFS-prover: scalable best-first tree search for llm-based automatic theorem proving. External Links: 2502.03438, Link Cited by: §I. [44] K. Yang and J. Deng (2019) Learning to prove theorems via interacting with proof assistants. CoRR abs/1905.09381. External Links: Link, 1905.09381 Cited by: §I, §VII-C. [45] 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 Advances in Neural Information Processing Systems, Vol. 36, p. 21573–21612. External Links: Link Cited by: §I-B. [46] K. Zheng, J. M. Han, and S. Polu (2021) MiniF2F: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110. Cited by: §I. -A Illustrative Example with Worst-Case Timing Requirements of Real-Time Tasks with Time Redundancy -A1 Extracted JSON and Informal Sketch for Illustrative Example Listing 3 presents the extracted json that is used for the Section VI. Listing 3: Structured extraction of Definition 1 and Claim 1 ⬇ [ "type": "definition", "identifier": "Definition 1", "formal_description": "statement": "W_i_k_i = W_i_0 + A_i_k_i", "variables": "W_i_k_i": "Worst case timing requirement of task tau_i in the presence of k_i faults", "W_i_0": "Failure-free computational requirement (WCET) of task tau_i", "A_i_k_i": "Worst case value of additional reprocessing time and overhead to tolerate k_i faults" , "assumptions": [ "Faults are transient or intermittent", "Faults are detected immediately upon occurrence" ], "conclusion": "Defines the total time a task requires to complete its execution and recovery actions." , "informal_sketch": "intuition": "The total time a task needs is its normal execution time plus the maximum possible time spent on fault detection, recovery, and re-execution.", "steps": [ "Identify the base execution time without faults W_i_0", "Calculate the maximum overhead A_i_k_i based on the specific redundancy technique used", "Sum them to find the total timing requirement" ], "key_insights": [ "Separates the functional execution time from the fault-tolerance overhead" ] , "dependencies": [] , "type": "claim", "identifier": "Claim 1", "formal_description": "statement": "W_i_k_i = k_i * (R_star + W_i_0) + W_i_0", "variables": "W_i_k_i": "Worst case timing requirement for retry", "k_i": "Number of faults", "R_star": "Task restart overhead (constant)", "W_i_0": "Failure-free WCET" , "assumptions": [ "Task must restart from the very beginning after every fault" ], "conclusion": "Calculates the WCTR for the Retry redundancy technique." , "informal_sketch": "intuition": "If a fault occurs, the task loses all progress and must restart. In the worst case, a fault occurs just before completion, requiring a full re-execution plus restart overhead for every fault.", "steps": [ "For each of the k_i faults, add the cost of a full restart (R_star) and a full re-execution (W_i_0)", "Add the final successful execution time (W_i_0)" ], "key_insights": [ "Retry is the most expensive technique because it discards all work done prior to the fault" ] , "dependencies": ["Definition 1"] ] Listing 4 presents the informal sketch that is used for the Section VI. This sketch is formatted as structured Rocq comments and serves as the direct input to the skeleton code generation phase. Listing 4: Informal sketch used as input to skeleton code generation ⬇ (* ====section==== definition Definition 1 Statement: W_i_k_i = W_i_0 + A_i_k_i Variables: W_i_k_i: Worst case timing requirement of task tau_i in the presence of k_i faults W_i_0: Failure-free computational requirement (WCET) of task tau_i A_i_k_i: Worst case value of additional reprocessing time and overhead to tolerate k_i faults Assumptions: 1. Faults are transient or intermittent 2. Faults are detected immediately upon occurrence Conclusion: Defines the total time a task requires to complete its execution and recovery actions. Intuition for generating code: The total time a task needs is its normal execution time plus the maximum possible time spent on fault detection, recovery, and re-execution. Steps for generating code: 1. Identify the base execution time without faults W_i_0 2. Calculate the maximum overhead A_i_k_i based on the specific redundancy technique used 3. Sum them to find the total timing requirement Key Insights: 1. Separates the functional execution time from the fault-tolerance overhead *) (* ====section==== claim Claim 1 Statement: W_i_k_i = k_i * (R_star + W_i_0) + W_i_0 Variables: W_i_k_i: Worst case timing requirement for retry k_i: Number of faults R_star: Task restart overhead (constant) W_i_0: Failure-free WCET Assumptions: 1. Task must restart from the very beginning after every fault Conclusion: Calculates the WCTR for the Retry redundancy technique. Intuition for generating code: If a fault occurs, the task loses all progress and must restart. In the worst case, a fault occurs just before completion, requiring a full re-execution plus restart overhead for every fault. Steps for generating code: 1. For each of the k_i faults, add the cost of a full restart (R_star) and a full re-execution (W_i_0) 2. Add the final successful execution time (W_i_0) Key Insights: 1. Retry is the most expensive technique because it discards all work done prior to the fault *) -B IEEE Xplore API query We queried IEEE Xplore using schedulability-analysis and real-time-systems keywords. ("schedulability analysis" OR "schedulability" OR "response time analysis" OR "response-time analysis") AND ("real-time system" OR "real-time systems" OR "real-time task" OR "real-time scheduling" OR "worst-case execution time") The API also allows us to restrict the search to specific conferences. For this purpose, we selected leading conferences in real-time systems and system automation. The conferences specified in our search are as follows: ("Real-Time Systems Symposium", "RTSS"), ("Real-Time and Embedded Technology and Applications Symposium", "RTAS"), ("Euromicro Conference on Real-Time Systems", "ECRTS"), ("Embedded Software", "EMSOFT"), ("Real-Time Computing Systems and Applications", "RTCSA"), ("Real-Time Networks and Systems", "RTNS"), ("Robotics: Science and Systems", "RSS"), ("Intelligent Robots and Systems", "IROS"), -C Prosa Documentation Details TABLE V: Role of major Prosa documentation modules. Module Role in Documentation Processing Behavior Core system semantics and basic concepts Model Task, processor, priority, and scheduler assumptions Analysis Reusable lemmas and intermediate proof developments Results Complete verified schedulability theorems and proof examples Implementation Executable instances and concrete schedulers Util Mathematical lemmas, helper functions, and tactics -D Pseudocode for skeleton code generation The pseudocode is presented in Algorithm 1 Algorithm 1 Phase 1: Skeleton Code Generation 1: Sketch sections S, retry budget MsM_s 2: Skeleton script P 3: P←∅P← ⊳ accumulated script 4: for each section si∈s_i do 5: Ci←RetrieveContext(si)C_i← RetrieveContext(s_i) 6: ki←InferKind(si)k_i← InferKind(s_i) 7: success←falsesuccess← false 8: for a←1a← 1 to MsM_s do 9: πi←BuildPrompt(si,Ci,P,ki) _i← BuildPrompt(s_i,C_i,P,k_i) 10: bi←GenerateBlock(πi)b_i← GenerateBlock( _i) 11: bi←Normalize(bi)b_i← Normalize(b_i) 12: if ¬CheckSkeletonRules(bi) CheckSkeletonRules(b_i) then 13: continue 14: end if 15: if ¬CheckAssumptions(bi,si) CheckAssumptions(b_i,s_i) then 16: continue 17: end if 18: P′←Concat(P,bi)P ← Concat(P,b_i) 19: if Compile(P′) Compile(P ) then 20: P←P′P← P 21: UpdateContext(P,bi) UpdateContext(P,b_i) 22: success←truesuccess← true 23: break 24: end if 25: end for 26: if success=falsesuccess=false then 27: return Failure(si) Failure(s_i) 28: end if 29: end for 30: return P -E Pseudocode for Batch Completion with Iterative Repair The pseudocode is presented in Algorithm 2 Algorithm 2 Phase 2a: Batch Completion with Compiler-Guided Repair 1: Skeleton sections ℬB, retry budget MbM_b 2: Completed script P 3: P←∅P← ⊳ completed script 4: for each section Bi∈ℬB_i do 5: if ¬HasAdmitted(Bi) HasAdmitted(B_i) then 6: P←Concat(P,Bi)P← Concat(P,B_i) 7: continue 8: end if 9: Ci←RetrieveContext(Bi)C_i← RetrieveContext(B_i) 10: πi←BuildCompletionPrompt(Bi,Ci,P) _i← BuildCompletionPrompt(B_i,C_i,P) 11: pi←GenerateProof(πi)p_i← GenerateProof( _i) 12: Bi′←ReplaceAdmitted(Bi,pi)B_i ← ReplaceAdmitted(B_i,p_i) 13: P′←Concat(P,Bi′)P ← Concat(P,B_i ) 14: success←Compile(P′)success← Compile(P ) 15: for a←1a← 1 to MbM_b do 16: if successsuccess then 17: break 18: end if 19: ei←ExtractError(P′)e_i← ExtractError(P ) 20: ρi←BuildRepairPrompt(Bi′,Ci,ei) _i← BuildRepairPrompt(B_i ,C_i,e_i) 21: pi←RepairProof(ρi)p_i← RepairProof( _i) 22: Bi′←ApplyRepair(Bi′,pi)B_i ← ApplyRepair(B_i ,p_i) 23: P′←Concat(P,Bi′)P ← Concat(P,B_i ) 24: success←Compile(P′)success← Compile(P ) 25: end for 26: if successsuccess then 27: P←P′P← P 28: MarkCompleted(Bi′) MarkCompleted(B_i ) 29: else 30: P←Concat(P,Bi)P← Concat(P,B_i) 31: MarkFailed(Bi) MarkFailed(B_i) 32: end if 33: end for 34: return P -F Illustrative Example with “Preemptively Scheduling Hard-Real-Time Sporadic Tasks on One Processor” [3] We illustrate another workflow of Prove-RT using a concrete schedulability analysis drawn from the RTS literature, starting with the extraction of intermediate representations and leading to the final machine-verified Prosa script. -F1 Source Material and Extraction We consider the paper “Preemptively Scheduling Hard-Real-Time Sporadic Tasks on One Processor” [3] as a representative example. From this paper, we extract the following definitions and lemma. In particular, the lemma Optimality of the Deadline Algorithm. serves as the main target, as it establishes the optimality of the deadline algorithm for sporadic task systems. This lemma relies on several preceding modeling definitions. Definition 1 (Sporadic Task Model). A sporadic task is defined as Ti=(ei,di,pi),T_i=(e_i,d_i,p_i), where eie_i is the execution time, did_i the relative deadline, and pip_i the minimum separation between consecutive requests, with ei≤die_i≤ d_i and ei≤pie_i≤ p_i. A task system is a finite set τ=T1,…,Tnτ=\T_1,…,T_n\. Definition 2 (Request Model). A request of task TiT_i released at time t0t_0 is represented as (i,t0)(i,t_0). It requires eie_i units of processor time in the interval [t0,t0+di),[t_0,t_0+d_i), so its absolute deadline is t0+dit_0+d_i. Definition 3 (Legal Request Sets and Feasibility). A request set is legal if two requests of the same task are separated by at least pip_i: |t1−t2|≥pi.|t_1-t_2|≥ p_i. A task system is feasible if every legal request set can be scheduled without missing deadlines. Thus, feasibility is a universal property over all legal sporadic arrivals. Definition 4 (Online Scheduling and Failure). An online scheduler decides at each time which active request executes. A request (i,t0)(i,t_0) is active at time t if t0≤t<t0+dit_0≤ t<t_0+d_i and it has not yet received eie_i units of execution. The scheduler reports failure when a request reaches its deadline without receiving enough execution. Definition 5 (Deadline Algorithm). The deadline algorithm selects, at each time, the active request with the earliest absolute deadline. For two active requests (i,t1)(i,t_1) and (j,t2)(j,t_2), it chooses (i,t1)(i,t_1) if t1+di<t2+dj.t_1+d_i<t_2+d_j. Ties are resolved using a fixed task-index order. Lemma 1 (Optimality of the Deadline Algorithm). The lemma states that the deadline algorithm is optimal for sporadic task systems. For any request set, if some feasible schedule exists, then the deadline algorithm also constructs one; otherwise, it reports failure. Therefore, τ is feasible⇔the deadline algorithm succeedsfor every legal request set.τ is feasible aligned &the deadline algorithm succeeds\\ &for every legal request set. aligned These results are automatically extracted and structured using LLM. Besides identifying the formal statement, variables, assumptions, and conclusion of each invariant, the extraction also produces an informal sketch. The Informal Sketch 5 was extracted for this proof construct Listing 5: Extracted Informal Sketch for Optimality of the Deadline Algorithm. ⬇ (* ====section==== definition Definition 1 Statement: A sporadic task task_i is a triple task_i = e_i, d_i, p_i where e_i, d_i, and p_i are positive integers, e_i <= d_i, and e_i <= p_i. A sporadic task system task_system is a finite set task_system = task_1, task_2, ..., task_n. Variables: task_i: sporadic task i task_system: set of sporadic tasks e_i: execution time of task_i d_i: relative deadline of task_i p_i: minimum separation between successive requests of task_i n: number of tasks Assumptions: 1. single processor 2. preemptive scheduling 3. discrete time model 4. e_i, d_i, p_i are positive integers 5. e_i <= d_i 6. e_i <= p_i Conclusion: Defines the sporadic task model and the task-system model. Intuition for generating code: Each sporadic task can release jobs at arbitrary times, but not too frequently. The parameter p_i prevents infinitely dense releases, while e_i and d_i describe how much processor time each released job needs and when it must complete. Steps for generating code: 1. Represent each task task_i by execution time e_i, deadline d_i, and minimum separation p_i. 2. Require e_i <= d_i so that each individual job can fit inside its own deadline window. 3. Require e_i <= p_i so that the task does not request more execution than its minimum inter-arrival spacing can plausibly support. 4. Collect all tasks into task_system. Key Insights: 1. The minimum separation p_i is the key distinction between sporadic and arbitrary aperiodic arrivals. 2. The model allows d_i > p_i, so jobs of the same task may have overlapping deadline windows. *) (* ====section==== definition Definition 2 Statement: Let P = lcm(p_1, p_2, ..., p_n). A request of task_i at time t_0 is represented by request_i_t_0 = i, t_0. The request requires e_i units of processor allocation in interval [t_0, t_0 + d_i). Variables: P: least common multiple of all minimum separations p_i request_i_t_0: request of task_i released at time t_0 t_0: release time of a request e_i: execution requirement of task_i d_i: relative deadline of task_i p_i: minimum separation of task_i Assumptions: 1. task_i belongs to task_system 2. t_0 >= 0 3. time is discrete Conclusion: Defines task requests and their execution windows. Intuition for generating code: A sporadic task generates individual requests or jobs. A request released at t_0 must receive e_i units of service before its absolute deadline t_0 + d_i. Steps for generating code: 1. Take a task task_i and release time t_0. 2. Construct request_i_t_0. 3. Set the absolute deadline to t_0 + d_i. 4. Require the scheduler to allocate e_i time units inside [t_0, t_0 + d_i). Key Insights: 1. Schedulability is checked over requests, not just over task parameters. 2. The absolute deadline is release_time plus relative deadline. *) (* ====section==== definition Definition 3 Statement: A set of requests request_set is schedulable iff there exists a processor schedule that allocates e_i time units to every request request_i_t_0 in request_set within [t_0, t_0 + d_i). A set request_set is legal iff for any two requests request_i_t_1 and request_i_t_2 of the same task, abs(t_1 - t_2) >= p_i. The task_system is feasible iff every legal request_set is schedulable. Variables: request_set: set of task requests request_i_t_0: request of task_i released at t_0 t_1: release time of one request t_2: release time of another request p_i: minimum separation of task_i task_system: sporadic task system Assumptions: 1. single processor 2. preemptive scheduling 3. all requests satisfy their task parameters Conclusion: Defines schedulability of a request set, legality of arrivals, and feasibility of a sporadic task system. Intuition for generating code: A request set is legal if it respects the sporadic separation constraints. A task system is feasible only if every possible legal arrival pattern can be scheduled without missing deadlines. Steps for generating code: 1. Check all pairs of requests of the same task. 2. If any two releases are closer than p_i, the request set is illegal. 3. If the request set is legal, ask whether a valid preemptive single-processor schedule exists. 4. The task system is feasible only when every legal request set has such a schedule. Key Insights: 1. Feasibility is a universal property over all legal arrival sequences. 2. The difficulty comes from the unbounded number of possible legal sporadic request sets. *) (* ====section==== definition Definition 4 Statement: An online scheduling algorithm U maps each request_set and time t to either a selected active request request_i_t_0, an idle decision, and optionally failure. A request request_i_t_0 is active at time t iff t_0 <= t < t_0 + d_i and the request has not yet received e_i units of processor allocation in [t_0, t). U reports failure at time t iff there exists request_i_t_0 such that t_0 + d_i = t and the request has received less than e_i units in [t_0, t). Variables: U: online scheduling algorithm request_set: set of requests presented to U t: current time request_i_t_0: request of task_i released at t_0 active: predicate indicating that a request is pending and before its deadline failure: event indicating a missed deadline Assumptions: 1. requests are presented to U at their release times 2. U is online and iterative 3. preemption is allowed at integer time boundaries Conclusion: Defines online scheduling, active requests, and failure. Intuition for generating code: At each time, the scheduler either runs one active request or idles. Failure occurs exactly when a request reaches its deadline without having received enough execution. Steps for generating code: 1. At each time t, identify all active requests. 2. Choose one active request to execute or leave the processor idle. 3. Update the amount of service received by the chosen request. 4. If any request reaches its deadline without receiving e_i service, report failure. Key Insights: 1. Failure is defined at the deadline boundary. 2. The active-request definition captures unfinished jobs that are still eligible to execute. *) (* ====section==== definition Definition 5 Statement: The deadline algorithm U allocates the processor at time t to the active request with the nearest absolute deadline. For active requests request_i_t_1 and request_j_t_2, U chooses request_i_t_1 over request_j_t_2 if t_1 + d_i < t_2 + d_j, or if t_1 + d_i = t_2 + d_j and i < j. Variables: U: deadline algorithm request_i_t_1: active request of task_i released at t_1 request_j_t_2: active request of task_j released at t_2 t_1_plus_d_i: absolute deadline of request_i_t_1 t_2_plus_d_j: absolute deadline of request_j_t_2 Assumptions: 1. preemptive scheduling 2. single processor 3. ties are broken by lower task index Conclusion: Defines the deadline-driven scheduling algorithm used throughout the paper. Intuition for generating code: The deadline algorithm is earliest-deadline-first with a deterministic tie-breaking rule. The request whose deadline is closest gets the processor. Steps for generating code: 1. At time t, collect all active requests. 2. Compute each active request’s absolute deadline. 3. Select the request with the smallest absolute deadline. 4. If two requests have the same absolute deadline, choose the one with smaller task index. Key Insights: 1. The algorithm is EDF specialized to the paper’s request model. 2. Tie-breaking does not affect whether failure occurs, but makes the schedule deterministic. *) (* ====section==== lemma Lemma 1 Statement: The deadline_algorithm_U is optimal for sporadic task systems. Given any request_set, U constructs a schedule for request_set if one exists; otherwise U reports failure at some time. Therefore task_system is feasible iff U constructs a schedule for every legal request_set. Variables: deadline_algorithm_U: earliest-deadline scheduling algorithm request_set: set of requests task_system: sporadic task system Assumptions: 1. single processor 2. preemptive scheduling 3. sporadic request model 4. legal request sets respect minimum separations Conclusion: EDF-style deadline scheduling is sufficient to decide feasibility over legal request sets. Intuition for generating code: For preemptive uniprocessor scheduling, always running the active job with the earliest deadline is optimal: if any schedule can meet all deadlines, the deadline algorithm can also meet them. Steps for generating code: 1. Consider any legal request set. 2. Run the deadline algorithm on that request set. 3. If any feasible schedule exists, the deadline algorithm also succeeds. 4. If the deadline algorithm fails, no feasible schedule exists for that request set. 5. Thus task_system is feasible exactly when the deadline algorithm never fails on any legal request set. Key Insights: 1. This lemma lets the paper focus on one canonical scheduler rather than all possible schedules. 2. It converts feasibility into absence of failure under the deadline algorithm. *) The extraction is also dependency-aware. For each invariant, we record its dependencies on previously introduced invariants, inducing a partial order for formalization. An invariant is formalized only after all dependencies have been processed. For example, Lemma 1 depends on Definitions 1–5, which must therefore be formalized first. Since Prosa/Rocq requires all referenced constructs to be defined before use, dependency-aware ordering is necessary for successful compilation. -F2 Retrieval-Augmented Generation Given the informal sketch of an invariant, the next step is to translate it into a Prosa script. To support this translation, we employ retrieval-augmented generation (RAG) over the Prosa codebase. We use the statement, conclusion, and intuition fields from the informal sketch as a joint query and retrieve the top-k results from two complementary sources: (i) example scripts that demonstrate similar constructs or proof patterns, and (i) documentation fragments describing the syntax, semantics, and usage conventions of relevant Prosa modules. Together, these provide the LLM with sufficient context to generate correct and idiomatic code. -F3 Skeleton Code Generation Using the retrieved context, we prompt the LLM to generate skeleton code—a structurally complete, type-checkable Prosa script in which all imports, section boundaries, type-class contexts, variable declarations, and definition bodies are fully specified, while every proof obligation is replaced by Admitted. Listing 6 shows the skeleton code generated for the motivating example. Listing 6: Skeleton code generated from the informal sketch. All structural elements are fully elaborated; the proof body is deferred via Admitted. ⬇ From mathcomp Require Import all_ssreflect. Require Import prosa.model.task.concept. Require Import prosa.model.task.arrival.sporadic. Require Import prosa.model.priority.edf. Require Import prosa.model.processor.ideal. Require Import prosa.model.readiness.basic. Require Import prosa.analysis.definitions.schedulability. Require Import prosa.analysis.facts.behavior.completion. Require Export prosa.results.edf.optimality. Section SporadicEDFOptimality. Context Task : TaskType ‘TaskCost Task ‘TaskDeadline Task ‘SporadicModel Task. Context Job : JobType ‘JobTask Job Task ‘JobArrival Job ‘JobCost Job ‘JobDeadline Job. Variable ts : seq Task. (* the sporadic task system tau = T_1,...,T_n *) Hypothesis H_job_deadline_def : forall j, job_deadline j = job_arrival j + task_deadline (job_task j). Definition valid_sporadic_task (tsk : Task) : Prop := [/\ 0 < task_cost tsk, 0 < task_deadline tsk, 0 < task_min_inter_arrival_time tsk, task_cost tsk <= task_deadline tsk & task_cost tsk <= task_min_inter_arrival_time tsk ]. Definition request_absolute_deadline (j : Job) : instant := job_arrival j + task_deadline (job_task j). (* = job_deadline j, by H_job_deadline_def *) Definition feasible : Prop := forall arr_seq : arrival_sequence Job, valid_arrival_sequence arr_seq -> (forall tsk, tsk ∈ ts -> respects_sporadic_task_model arr_seq tsk) -> exists sched : schedule (ideal.processor_state Job), valid_schedule sched arr_seq /\ all_deadlines_of_arrivals_met arr_seq sched. Definition online_failure_at (arr_seq : arrival_sequence Job) (sched : schedule (ideal.processor_state Job)) (t : instant) : Prop := exists j, arrives_in arr_seq j /\ job_deadline j = t /\ ~~ completed_by sched j t. Definition deadline_algorithm_U (sched : schedule (ideal.processor_state Job)) : Prop := EDF_schedule sched. Lemma deadline_algorithm_optimal : feasible <-> (forall arr_seq : arrival_sequence Job, valid_arrival_sequence arr_seq -> (forall tsk, tsk ∈ ts -> respects_sporadic_task_model arr_seq tsk) -> exists sched : schedule (ideal.processor_state Job), valid_schedule sched arr_seq /\ all_deadlines_of_arrivals_met arr_seq sched /\ deadline_algorithm_U sched). Proof. Admitted. End SporadicEDFOptimality. The skeleton maps each extracted section to a corresponding Prosa construct. Definition 1 is encoded as valid_sporadic_task, using task_cost, task_deadline, and task_min_inter_arrival_time for eie_i, did_i, and pip_i. Definition 2 is encoded as request_absolute_deadline, representing the absolute deadline t0+dit_0+d_i. Definition 3 is encoded as feasible, which quantifies over all legal arrival sequences. Definition 4 is encoded as online_failure_at, capturing missed deadlines, and Definition 5 is encoded as deadline_algorithm_U, identified with Prosa’s EDF_schedule. Lemma 1 is encoded as deadline_algorithm_optimal, stating that feasibility is equivalent to success of the deadline algorithm on every legal request set. The surrounding type-class context, including TaskType, JobType, and TaskCost, connects these constructs to Prosa’s scheduling framework. The Admitted. directive is used only as a temporary placeholder, allowing the skeleton to type-check before the proof is synthesized, with the final proof expected to rely on Prosa’s EDF_optimality theorem. -F4 Proof Completion In the final phase, we prompt the LLM to discharge the Admitted obligations using the complete skeleton, retrieved RAG context, and an instruction to complete a specific proof block. Providing the full skeleton gives the model access to surrounding definitions, instances, and auxiliary lemmas, improving proof generation. For this example, the LLM produces the following proof in Listing 7: Listing 7: Completed proof for the Optimality of the Deadline Algorithm ⬇ Lemma deadline_algorithm_optimal : feasible <-> (forall arr_seq : arrival_sequence Job, valid_arrival_sequence arr_seq -> (forall tsk, tsk ∈ ts -> respects_sporadic_task_model arr_seq tsk) -> exists sched : schedule (ideal.processor_state Job), valid_schedule sched arr_seq /\ all_deadlines_of_arrivals_met arr_seq sched /\ deadline_algorithm_U sched). Proof. rewrite /feasible /deadline_algorithm_U. split. - move=> FEAS arr_seq VALID SPORADIC. apply: EDF_optimality. have [sched [VALID_SCHED DEADLINES_MET]] := FEAS arr_seq VALID SPORADIC. by exists sched. - move=> EDF_FEAS arr_seq VALID SPORADIC. have [sched [VALID_SCHED [DEADLINES_MET EDF_SCHED]]] := EDF_FEAS arr_seq VALID SPORADIC. by exists sched. Qed. The proof follows the two directions of the equivalence. First, rewrite /feasible /deadline_algorithm_U unfolds the extracted definitions, reducing the statement to the relationship between general feasibility and existence of an EDF schedule. In the forward direction, the assumption FEAS provides some valid schedule that meets all deadlines for any legal arrival sequence. The proof then applies EDF_optimality, which states that if such a feasible schedule exists, then an EDF schedule also exists. In the reverse direction, the assumption already provides a valid schedule that meets all deadlines and additionally satisfies EDF_schedule. Since feasibility only requires the existence of some valid schedule meeting all deadlines, the EDF-specific condition is discarded. Thus, the completed proof shows that the extracted lemma deadline_algorithm_optimal is a valid Prosa formalization of the paper’s claim that the deadline algorithm is optimal for preemptive uniprocessor sporadic task systems. This example demonstrates how our pipeline systematically transforms informal real-time scheduling results into machine-verified Prosa proofs through a structured sequence of extraction, retrieval-augmented skeleton generation, and targeted proof completion. -G Distribution of system invariants and their number of dependencies in the generated System Invariant Dataset Figure 6 shows the distribution of the total number of invariants per sketch, defined as the target invariant plus its associated dependencies. The frequency decreases as the number of dependencies increases, indicating that highly dependent invariants are less common in the extracted corpus. Fig. 6: Distribution of system invariants and their dependencies. -H Fine-Grained Mapping from Raw Sketch Kinds to Rocq Keywords Table VI presents the complete mapping from raw sketch kinds to their corresponding Rocq keywords, along with the rationale used in our normalization process. TABLE VI: Fine-grained mapping from raw sketch kinds to Rocq keywords. Raw Sketch Kind Rocq Keyword Reason Definition family definition Definition Direct equivalent formula Definition A named mathematical formula = constant definition equation Definition A named equation = defined constant/relation implicit_definition Definition Implicitly defined concept derived_definition Definition Derived from other definitions foundational_equation Definition Named base equation = constant rta_equation Definition Response-time analysis equation = named bound constant calculation_formula Definition A formula used in calculation = named constant derived_formula Definition Derived formula = defined constant resource_planning_formula Definition Formula for planning = named constant objective_function Definition Optimization objective = a function definition optimization_objective Definition Same as objective_function derived_function Definition Derived non-recursively (not Fixpoint) function Definition Non-recursive function formulation Definition Mathematical formulation = a definition task_set_definition Definition Explicit definition of a task set informal_definition Definition Informal but definitional in nature Fixpoint family algorithm Fixpoint Algorithms are recursive = Fixpoint algorithmic_sketch Fixpoint Sketch of a recursive algorithm informal_algorithmic_sketch Fixpoint Informal version of algorithmic_sketch algorithm_sketch Fixpoint Same as algorithmic_sketch algorithm_component Fixpoint Part of a recursive algorithm algorithm_definition Fixpoint Defines a recursive algorithm algorithm_description Fixpoint Describes an algorithm algorithmic_derivation Fixpoint Algorithmically derived result algorithmic_definition Fixpoint Formally defined algorithm transformation_algorithm Fixpoint An algorithm that transforms its input method Fixpoint Computational method = procedure procedure Fixpoint Explicit computational procedure heuristic Fixpoint Iterative/recursive computational procedure recurrence Fixpoint Recurrence relation = recursive definition Lemma family lemma Lemma Direct equivalent claim Lemma A claim is an auxiliary provable fact proposition Lemma Proposition = Lemma in Rocq convention observation Lemma An observation is an informal lemma property Lemma A provable proposition statement Lemma A mathematical statement to be proved formal_statement Lemma Formal version of a statement condition Lemma A provable condition/predicate constraint Lemma Proved inequality or bound calculation Lemma Result of a calculation = proved equality schedulability_test Lemma Decidable test = proved as lemma derived_test Lemma A test derived from other results optimization_constraint Lemma Proved inequality/bound optimization_claim Lemma Claim about an optimisation application Lemma Instantiation of a result invariant Lemma System/loop invariants proved as lemmas remark Lemma Remarks are informal lemmas fact Lemma A mathematical fact result Lemma A proved result restriction Lemma A restriction = conditional lemma conjecture Lemma Unproved; placeholder with Admitted property/constraint Lemma Combined property/constraint problem Lemma Decision/optimisation problem rule Lemma Inference rule = proved as lemma optimization_problem Lemma Proved bound/property schedulability_condition Lemma Schedulability condition = proved predicate problem_statement Lemma Problem stated formally inequality Lemma A proved inequality known_result Lemma Existing proved result principle Lemma e.g. scheduling principle = proved property derived_rta Lemma Response-time bounds are proved, not defined extension Lemma Extends an existing lemma transformation Lemma Proved equivalence under transformation refinement Lemma Proved relationship between specifications informal_sketch Lemma Informal sketch of a proof obligation informal Lemma Generic informal mathematical statement policy Lemma Scheduling policy property = provable proposition incomplete_malformed_statement Lemma Safe fallback Theorem / Corollary / Hypothesis families theorem Theorem Direct equivalent corollary Corollary Direct equivalent hypothesis Hypothesis Direct equivalent assumption Hypothesis Explicit assumption in a Rocq Section context TABLE VI: Fine-grained mapping from raw sketch kinds to Rocq keywords (continued).

Instant research discovery