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

# Prove-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs
Source: [https://arxiv.org/html/2608.12762](https://arxiv.org/html/2608.12762)
Sadat Shahriyar1, Shareef Ahmed2, Abdullah Al Arafat1Affiliation: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 inProsa/Rocqoffers 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 generatingProsa/Rocqscripts for mechanized theorem provers\. However, state\-of\-the\-art LLMs often lack theProsa\-specific knowledge required to correctly use its modeling abstractions and proof patterns\.

This paper introducesProve\-RT, an LLM\-assisted framework for generatingProsa/Rocqscripts to mechanize schedulability analyses in real\-time systems literature\.Prove\-RTguides generation through dependency\-aware informal sketches, retrieval from processedProsadocumentation, staged skeleton generation, and proof completion\. We construct a mechanization\-oriented corpus from1,1911,191real\-time systems papers, containing13,13413,134informal sketches with dependency information\. On a curated evaluation set, direct prompting of state\-of\-the\-art LLMs fails to reliably generate validProsamechanizations, whereasProve\-RTachieves a success rate of44\.7%44\.7\\%\. These results show that retrieval\-guided and staged LLM assistance can improve automated mechanization of schedulability analysis inProsa/Rocq\.

## IIntroduction

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](https://arxiv.org/html/2608.12762#bib.bib3),[8](https://arxiv.org/html/2608.12762#bib.bib2),[29](https://arxiv.org/html/2608.12762#bib.bib4),[10](https://arxiv.org/html/2608.12762#bib.bib5)\]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](https://arxiv.org/html/2608.12762#bib.bib18)developed the first mechanized theorem prover,Prosa, for real\-time systems\.Prosaprovides aRocq\[[38](https://arxiv.org/html/2608.12762#bib.bib9)\]\-based foundation for mechanized schedulability analysis, offering a more rigorous approach for verifying the correctness of pen\-and\-paper proofs\.Prosais 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 onRocq,Prosaenables 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, aProsa\-basedRocqtool for certifying CAN schedulability\-analysis results, required 18,852 lines ofRocqcode, excluding theProsaproofs that it reused\[[18](https://arxiv.org/html/2608.12762#bib.bib6)\]\. Similarly, integratingProsa’s verified schedulability analysis into the RT\-CertiKOS verified operating\-system kernel required 4,135 lines ofRocqfor the connection alone, including 1,900 lines for the translation interface toProsa\[[20](https://arxiv.org/html/2608.12762#bib.bib7)\]\. Beyond initial development costs, mechanized proofs also incur maintenance costs: for instance,[7](https://arxiv.org/html/2608.12762#bib.bib8)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 althoughProsaprovides 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](https://arxiv.org/html/2608.12762#bib.bib9),[30](https://arxiv.org/html/2608.12762#bib.bib10),[12](https://arxiv.org/html/2608.12762#bib.bib12),[40](https://arxiv.org/html/2608.12762#bib.bib11)\]in general cases, a growing body of work has explored automated theorem proving and proof automation using machine learning\[[5](https://arxiv.org/html/2608.12762#bib.bib19),[16](https://arxiv.org/html/2608.12762#bib.bib20),[6](https://arxiv.org/html/2608.12762#bib.bib22),[14](https://arxiv.org/html/2608.12762#bib.bib21),[34](https://arxiv.org/html/2608.12762#bib.bib23),[35](https://arxiv.org/html/2608.12762#bib.bib24),[11](https://arxiv.org/html/2608.12762#bib.bib25)\]\. 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 introduceProve\-RT, a novel*large\-language\-model*\(LLM\)\-assisted framework for generating mechanizedProsaproofs for schedulability analyses whose correctness can be verified mechanically\.*It is noteworthy that, beyond mechanizing existing schedulability analyses,Prove\-RTmay also facilitate the trustworthy use of generative AI for developing new schedulability analyses\. As generative AI has shown promise across many scientific disciplines\[[43](https://arxiv.org/html/2608.12762#bib.bib37),[32](https://arxiv.org/html/2608.12762#bib.bib38),[36](https://arxiv.org/html/2608.12762#bib.bib39)\],Prove\-RTcan 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, generatingProsascripts 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 ofProsaabstractions and proof patterns; \(ii\) a formalization gap between structurally non\-mechanized schedulability analyses andProsa’s explicit proof structure; and \(iii\) the complexity in the structure of schedulability lemmas/theorems compared to mathematical theorem\-proving tasks\. These challenges are elaborated in Section[II](https://arxiv.org/html/2608.12762#S2)\. To overcome them,Prove\-RTincrementally mechanizes schedulability analyses through staged formalization, dependency\-aware proof construction, and retrieval\-augmented grounding using RTS knowledge andProsadocumentation\.

In summary, this paper makes the following contributions:

- •We introduceProve\-RT, a framework for assisting the mechanization of schedulability analyses inProsa/Rocq\. To the best of our knowledge,Prove\-RTis the first LLM\-assisted framework targeting theProsa\-based mechanization of RTS analysis\.
- •We develop a benchmark from1,1911,191real\-time systems papers, comprising13,13413,134mechanization\-oriented informal sketches and correspondingProsa/Rocqscript 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 generatingProsa/Rocqscripts 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[II](https://arxiv.org/html/2608.12762#S2)elaborates on the core challenges while mechanizing schedulability analysis withProsa\. Section[III](https://arxiv.org/html/2608.12762#S3)provides background onProsaand reviews related work\. Section[IV](https://arxiv.org/html/2608.12762#S4)introduces the notation used throughout the paper and formalizes the problem statement\. Section[V](https://arxiv.org/html/2608.12762#S5)presents the design ofProve\-RT\. Section[VII](https://arxiv.org/html/2608.12762#S7)describes the construction of the system invariant dataset, the evaluation baselines and metrics, and the implementation details\. Section[VI](https://arxiv.org/html/2608.12762#S6)provides an example on how the framework works\. Section[VIII](https://arxiv.org/html/2608.12762#S8)presents the evaluation ofProve\-RT\. Finally, Section[IX](https://arxiv.org/html/2608.12762#S9)concludes the paper by discussing the limitations ofProve\-RTand outlining directions for future work\.

## IIChallenges 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 inProsa/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](https://arxiv.org/html/2608.12762#bib.bib42),[46](https://arxiv.org/html/2608.12762#bib.bib43),[1](https://arxiv.org/html/2608.12762#bib.bib44),[44](https://arxiv.org/html/2608.12762#bib.bib32),[2](https://arxiv.org/html/2608.12762#bib.bib45),[41](https://arxiv.org/html/2608.12762#bib.bib46)\], which provide many examples of theorem statements, proof scripts, and reusable mathematical libraries\. In contrast, public data for mechanized schedulability analysis is very limited\. TheProsalibrary 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 learnProsa\-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 byProsa\. 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\. AProsa/Rocqdevelopment 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 existingProsaabstractions 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 inProsacan span hundreds of lines\. This creates a substantial burden on the LLM’s context handling and reasoning capabilities\.

Beyond the complexity of individual lemmas,Prosais 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\.

## IIIPreliminaries and Related Work

In this section, we will discuss the necessaryProsabackground and the related works on mechanized theorem provers and script generation\.

### III\-ABackground onProsa

Prosa\[[9](https://arxiv.org/html/2608.12762#bib.bib18)\]is aRocqlibrary for mechanized schedulability analysis of RTS\. It formalizes real\-time scheduling concepts as Gallina \(i\.e\.,Rocqspecification language\) definitions and establishes schedulability results as machine\-checked lemmas and theorems\. SinceProsais built inRocq, aProsascript follows the standardRocqdevelopment 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 ofProsadevelopments is their reliance on explicit proof context\. ASectiongroups together variables, hypotheses, and type\-class constraints that are shared by the definitions and lemmas inside it\.ProsausesRocqtype classes to represent reusable modeling assumptions, such as task parameters, job parameters, scheduling policies, and system properties\. Although these assumptions may be inferred automatically byRocqvia type\-class resolution, the required instances must be available in the current context or imported environment for the script to type\-check\.

Rocqfollows a forward\-referencing discipline: every definition, hypothesis, lemma, theorem, and imported module must be introduced before it is used\. Thus, a validProsadevelopment 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 correctProsascripts\.

We briefly summarize theRocq/Prosanotions that are needed to follow the rest of the paper\.

- •Proof scriptis theRocqsource code used to express a formal development\. InProsa, a proof script contains imports, definitions, assumptions, lemmas, theorems, and tactic\-based proofs for schedulability analysis\.
- •Proof environmentrefers 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 contextrefers to the local information available at a particular point in a proof\. InProsa, this often includes variables, hypotheses, task and job parameters, scheduling assumptions, and type\-class instances introduced inside a section\.
- •Proof goalis the proposition that remains to be proved\. A schedulability theorem inProsamay generate one or more proof goals involving task assumptions, workload bounds, interference bounds, or response\-time guarantees\.
- •Proof tacticis a command used to advance a proof by transforming the current goal into simpler subgoals or by solving it directly\. CommonRocqtactics includeintros,apply,rewrite,simpl, andlia\.
- •Proof stepis one application of a proof tactic\. Each proof step changes the current proof state and moves the proof closer to completion\.
- •Proof stateis 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 resolutionisRocq’s mechanism for automatically finding required instances of abstract interfaces\.Prosauses type classes to represent reusable modeling assumptions, such as job costs, task parameters, arrival information, and scheduling properties\.
- •Proof obligationis a statement that must be proved before a development is complete\. Lemmas, theorems, and corollaries introduce proof obligations, whereas definitions mainly introduce formal objects\.
- •Compilationis the process of checking aRocq/Prosafile\. 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\.

### III\-BRelated 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 asRocq\[[38](https://arxiv.org/html/2608.12762#bib.bib9)\]\(commonly known as Coq\), Isabelle\[[30](https://arxiv.org/html/2608.12762#bib.bib10)\], Agda\[[40](https://arxiv.org/html/2608.12762#bib.bib11)\], and Lean\[[12](https://arxiv.org/html/2608.12762#bib.bib12)\], have been widely used in the verification community\. These proof assistants have supported the verification of a broad range of software systems\. For example,Rocqhas been used to verify the CompCert C compiler\[[26](https://arxiv.org/html/2608.12762#bib.bib13)\], a lightweight relational database management system\[[28](https://arxiv.org/html/2608.12762#bib.bib15)\], and distributed systems through the Verdi framework\[[42](https://arxiv.org/html/2608.12762#bib.bib16)\]\. Isabelle/HOL has been used to verify the seL4 operating\-system kernel\[[24](https://arxiv.org/html/2608.12762#bib.bib14)\]\. More recently, Lean has been used to formalize and verify neural networks through TorchLean\[[19](https://arxiv.org/html/2608.12762#bib.bib17)\]\.

In real\-time systems,Prosaprovides aRocq\-based foundation for mechanized schedulability analysis\[[9](https://arxiv.org/html/2608.12762#bib.bib18)\]\. 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 usedProsato 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](https://arxiv.org/html/2608.12762#bib.bib8),[18](https://arxiv.org/html/2608.12762#bib.bib6),[4](https://arxiv.org/html/2608.12762#bib.bib40),[27](https://arxiv.org/html/2608.12762#bib.bib1),[33](https://arxiv.org/html/2608.12762#bib.bib41)\]\. 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](https://arxiv.org/html/2608.12762#bib.bib19),[16](https://arxiv.org/html/2608.12762#bib.bib20),[6](https://arxiv.org/html/2608.12762#bib.bib22),[14](https://arxiv.org/html/2608.12762#bib.bib21),[34](https://arxiv.org/html/2608.12762#bib.bib23),[35](https://arxiv.org/html/2608.12762#bib.bib24),[11](https://arxiv.org/html/2608.12762#bib.bib25)\]\. More recently, large language models \(LLMs\) have shown promise in generating formal proofs and assisting interactive theorem proving\[[21](https://arxiv.org/html/2608.12762#bib.bib26),[23](https://arxiv.org/html/2608.12762#bib.bib27),[45](https://arxiv.org/html/2608.12762#bib.bib30),[22](https://arxiv.org/html/2608.12762#bib.bib28),[31](https://arxiv.org/html/2608.12762#bib.bib29),[39](https://arxiv.org/html/2608.12762#bib.bib31)\]\. 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 generateProsaproofs for mechanized schedulability analysis from real\-time systems papers\.

## IVFramework Model and Problem Statement

### IV\-AFramework Model

We first define the main objects used throughout theProve\-RTpipeline\.

Schedulability Analysis \(AA\)\.LetAAbe 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 standardRocqtactic\-generation tasks,AAis 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 \(II\)\.We use the term*system invariant*to refer to any mechanization\-relevant construct inAAthat must be represented in the finalProsa/Rocqdevelopment\. 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 byI=\{i1,i2,…,in\}\.I=\\\{i\_\{1\},i\_\{2\},\\ldots,i\_\{n\}\\\}\.

Informal Sketch \(\{Kj\}\\\{K\_\{j\}\\\}\)\.An informal sketchKjK\_\{j\}describes the statement of the invariantiji\_\{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 generatedProsa/Rocqscript\. Each invariantij∈Ii\_\{j\}\\in Iis associated with an informal sketchKjK\_\{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\}\)\\in Dmeans that invariantiji\_\{j\}depends onipi\_\{p\}\. Thus,ipi\_\{p\}must appear earlier thaniji\_\{j\}in the generatedProsa/Rocqscript\. The DAG, therefore, defines the order in which invariants should be formalized\. This ordering is required becauseRocqis forward\-referencing: all definitions, assumptions, lemmas, theorems, and imports must be introduced before they are used\.

ProsaDocumentation Corpus \(PP\)\.LetPPbe the processedProsadocumentation corpus\.PPcontains documentation fragments, definitions, assumptions, reusable lemmas, and example proof structures extracted from theProsalibrary\. For each invariantiji\_\{j\}, the retrieval module selects a relevant subsetRj⊆PR\_\{j\}\\subseteq Pto provide the library\-specific context needed for script generation\.

The generated script is built incrementally according to the dependency order induced byGDG\_\{D\}\.

### IV\-BProblem Statement

Given a schedulability analysisAAand a processedProsadocumentation corpusPP, the goal ofProve\-RTis to generate a dependency\-orderedProsa/RocqscriptSSthat mechanizes the schedulability analysis and compiles under theProsa/Rocqenvironment as:

M:\(A,P\)→S,M:\(A,P\)\\rightarrow S,whereMMdenotes theProve\-RTgeneration pipeline andS=\{s1,s2,…,sn\}S=\\\{s\_\{1\},s\_\{2\},\\ldots,s\_\{n\}\\\}is the generatedProsa/Rocqscript\. Each code blocksj∈Ss\_\{j\}\\in Sis intended to formalize the corresponding system invariantij∈Ii\_\{j\}\\in I\.

A successful output must satisfy three requirements\. First, each generated code blocksjs\_\{j\}must correctly represent the corresponding extracted invariantiji\_\{j\}\. Second, the ordering of code blocks inSSmust respect the dependency graphGD=\(I,D\)G\_\{D\}=\(I,D\), so that every prerequisite invariant is introduced before any invariant that depends on it\. Third, the final scriptSSmust compile under theProsa/Rocqenvironment\.

We decompose this objective into two subproblems\.

Skeleton Generation \(viaMskelM\_\{\\mathrm\{skel\}\}\)\.The first subproblem is*skeleton generation*\. For each invariantiji\_\{j\}, the skeleton\-generation module uses the informal sketchKjK\_\{j\}, the retrievedProsacontextRjR\_\{j\}, the dependency graphGDG\_\{D\}, and the partialProsa/Rocqscript already generated for earlier invariants, denoted byS<jS\_\{<j\}, to produce a structurally validProsa/Rocqcode block:

Mskel:\(Kj,Rj,GD,S<j\)→sj\.M\_\{\\mathrm\{skel\}\}:\(K\_\{j\},R\_\{j\},G\_\{D\},S\_\{<j\}\)\\rightarrow s\_\{j\}\.
After the skeleton\-generation stage, some generatedProsa/Rocqfragments contain proof\-bearing constructs, such as lemmas, theorems, or corollaries, whose proof bodies were intentionally left asAdmitted\.We refer to these unfinished proof bodies as deferred proof obligations\. The proof\-completion stage attempts to replace eachAdmitted\.placeholder with a validRocqproof\.

For each deferred proof associated withsjs\_\{j\}, the proof\-completion module takes the current partial scriptS<jS\_\{<j\}, the corresponding informal sketchKjK\_\{j\}, and the retrievedProsacontext as inputRjR\_\{j\}, and generates a proof fragmentπj\\pi\_\{j\}intended to replace theAdmitted\.placeholder\.

Proof Completion \(viaMproofM\_\{\\mathrm\{proof\}\}\)\.The second subproblem is*proof completion*\. For each deferred proof insjs\_\{j\}, the proof\-completion module uses the current partial scriptS<jS\_\{<j\}, the informal sketchKjK\_\{j\}, and the retrievedProsacontextRjR\_\{j\}to generate a proof fragmentπj\\pi\_\{j\}:

Mproof:\(S<j,sj,Kj,Rj\)→πj\.M\_\{\\mathrm\{proof\}\}:\(S\_\{<j\},s\_\{j\},K\_\{j\},R\_\{j\}\)\\rightarrow\\pi\_\{j\}\.
The generated proof fragmentπj\\pi\_\{j\}is intended to replace the correspondingAdmittedplaceholder\. It is accepted only if the resultingProsa/Rocqscript is checked successfully by theRocqcompiler\. If compilation fails, compiler feedback or proof\-state information is used to guide repair\.

Thus, the problem addressed byProve\-RTis broader than next\-tactic prediction\. It requires transforming a real\-time systems schedulability analysis into a dependency\-orderedProsa/Rocqscript that can be mechanically checked by the proof assistant\.

## VProve\-RT Framework

Prove\-RTconsists of five stages: \(1\) Extracting system invariants, informal sketches, and dependency graph from formally written schedulability analysis; \(2\) Processing theProsadocumentation 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](https://arxiv.org/html/2608.12762#S5.F1)illustrates an overview of theProve\-RT\.

![Refer to caption](https://arxiv.org/html/2608.12762v1/system_diagram.png)Fig\. 1:Overview of the proposedProsa/Rocqproof\-generation pipeline\.### V\-ASystem Invariant Extraction

Extraction of Invariants and Sketches\.The first stage ofProve\-RTtransforms the input, schedulability analysisAA, into the intermediate representation required for mechanization, consisting of a set of system invariantsII, their corresponding informal sketches\{Kj\}\\\{K\_\{j\}\\\}, and a dependency graphGD=\(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 forProsa/Rocqgeneration may appear in different forms, including prose explanations, equations, definitions, lemmas, theorems, claims, or corollaries\.

To facilitate this process,Prove\-RTfirst prompts an LLM to identify candidate system invariants from schedulability testAA\. 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 invariantij∈Ii\_\{j\}\\in I, the LLM generates an informal sketchKjK\_\{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](https://arxiv.org/html/2608.12762#LST4)in Appendix[\-A1](https://arxiv.org/html/2608.12762#A0.SS1.SSS1)\.

Construction of Dependency Graph\.The extracted dependency information is used to construct the dependency graphGD=\(I,D\)G\_\{D\}=\(I,D\)\. For each invariantiji\_\{j\}, the LLM identifies other invariants that must be established beforeiji\_\{j\}can be formalized\. Each such relation is represented as an edge inDD\. The extracted invariants are then ordered according to this graph so that, when theProsa/Rocqscript is generated, prerequisites are introduced before the constructs that depend on them\. The resulting unit\-level informal sketches, ordered byGDG\_\{D\}, form the primary input to the subsequent stages ofProve\-RT\.

### V\-BProsaDocumentation Processing

The second stage ofProve\-RTconstructs the processedProsadocumentation corpusPPused for retrieval\. This stage is necessary because direct LLM\-based generation ofProsa/Rocqscripts is difficult without library\-specific context\. TheProsalibrary relies on domain\-specific abstractions, type\-class assumptions, reusable lemmas, and proof conventions that are often not available to a pretrained model\. Thus, theProsadocumentation is processed into retrieval\-ready fragments so that later stages can retrieve relevant proof constructs for each invariantiji\_\{j\}\.

TheProsadocumentation is organized into six main modules:Analysis,Behavior,Implementation,Model,Results, andUtil\. These modules are used to guide the construction ofPP\. In particular, theResultsmodule 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 theAnalysisandResultsmodules, 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](https://arxiv.org/html/2608.12762#S5.SS3)\.

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 corpusPP\. During retrieval,Prove\-RTselects a relevant subsetRj⊆PR\_\{j\}\\subseteq Pfor each invariantiji\_\{j\}, which provides the LLM withProsa\-specific context for generating the correspondingProsa/Rocqcode blocksjs\_\{j\}\.

### V\-CRetrieval Process

Query Construction\.The retrieval stage constructs the contextRj⊆PR\_\{j\}\\subseteq Pfor each invariantiji\_\{j\}\. Given the informal sketchKjK\_\{j\}, the goal is to retrieve the most relevant fragments from the processedProsadocumentation corpusPPso 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 byGDG\_\{D\}, we process the sketches one invariant at a time\. For each invariantiji\_\{j\}, its corresponding sketchKjK\_\{j\}is used as the retrieval unit\.

For each informal sketch unitKjK\_\{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\-kklist for each component\. The retrieved candidates are then merged, and the highest\-scoring documentation sections are selected as the retrieval contextRjR\_\{j\}\.

Dependency Recovery for Proof\-Oriented Modules\.For candidates retrieved from theAnalysisorResultsmodules, an additional syntax\-aware dependency recovery step is applied before adding them toRjR\_\{j\}\. These modules contain proof\-oriented files in which later sections often rely on earlier definitions, hypotheses, lemmas, or typeclass contexts\. SinceRocqfollows a forward\-referencing discipline, a section with indexNNcan depend only on preceding sections with indices from00toN−1N\-1within the same file\.Prove\-RTexploits 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 theProof\.keyword are treated as the strongest signals because they appear in the type\-level statement of the declaration\. Explicit references following tactics such asapplyandrewriteare 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\)=\\max\\bigl\(\\alpha\\cdot\\mathbf\{F\}\[x\\in Z\_\{A\}\],\\;\\beta\\cdot\\mathbf\{F\}\[x\\in Z\_\{B\}\],\\;\\gamma\\cdot\\mathbf\{F\}\[x\\in Z\_\{C\}\]\\bigr\),Here,ZAZ\_\{A\},ZBZ\_\{B\}, andZCZ\_\{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α\\alpha,β\\beta, andγ\\gammaare weighting coefficients assigned to these zones, withα\>β\>γ\\alpha\>\\beta\>\\gammato 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 inRjR\_\{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\-kkmatching sections are retrieved, and used directly without additional dependency recovery\.

### V\-DSkeleton Code Generation

The skeleton\-generation stage addresses the first subproblem defined in Section[IV](https://arxiv.org/html/2608.12762#S4)\. For each invariantiji\_\{j\}, it generates a structurally validProsa/Rocqcode blocksjs\_\{j\}using the invariant’s informal sketchKjK\_\{j\}, the retrieved contextRjR\_\{j\}, the dependency graphGDG\_\{D\}, and the partial scriptS<jS\_\{<j\}generated for earlier invariants\.

This stage deliberately separates structure generation from proof generation\. Generating the correct type signature of aProsa/Rocqconstruct, 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 bycoqc, allowingProve\-RTto detect structural errors before attempting proof synthesis\.

Prompt Construction\.For each invariantiji\_\{j\}, we construct the skeleton\-generation prompt from four inputs: the informal sketchKjK\_\{j\}, the retrievedProsacontextRjR\_\{j\}, the dependency graphGDG\_\{D\}, and the partial scriptS<jS\_\{<j\}\. These components provide the model with the relevant library context, examples ofProsastructure, and the current proof context\. The informal sketchKjK\_\{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 blocksjs\_\{j\}is structurally meaningful\. First,proof\-skeleton ruleis enforced where every proof\-bearing construct must be generated with a deferred proof obligation usingAdmitted\., 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 rulesare 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 fromKjK\_\{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 blocksjs\_\{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 generationValidation and Retry\.After each generation attempt, the produced skeletonsjs\_\{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 scriptS<jS\_\{<j\}and the resulting script is compiled withcoqc\. This verifies structural validity and type correctness\.

Non\-proof\-bearing constructs are accepted directly because they do not open aProof\.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\-ESkeleton Code Completion

After skeleton generation, each code blocksjs\_\{j\}may contain proof\-bearing constructs whose proof bodies are deferred usingAdmitted\.The goal of the completion stage is to generate a proof fragmentπj\\pi\_\{j\}that replaces each deferred proof and makes the resultingProsa/Rocqscript compile\. For each deferred proof, the completion module uses the current partial scriptS<jS\_\{<j\}, the corresponding informal sketchKjK\_\{j\}, and the retrievedProsacontextRjR\_\{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\-RTprompts LLM to generate the full proof body for a deferred proof in one response\. The generated proof fragmentπj\\pi\_\{j\}replaces the correspondingAdmitted\.placeholder insjs\_\{j\}, and the resulting partial script is then checked with theRocqcompiler\. 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 asAxiom,Parameter,Parameters,Conjecture,Conjectures,Admitted,admit, andAbort\. 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 fromProsaor 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\-RTenters 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 sketchKjK\_\{j\}and the retrieved contextRjR\_\{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

## VIIllustrative Example

We illustrate the end\-to\-end workflow ofProve\-RTusing a concrete schedulability analysis drawn from the RTS literature, starting with the extraction of intermediate representations and leading to the final machine\-verifiedProsascript\.

### VI\-ASource Material and Extraction

We consider the paper*“Worst\-Case Timing Requirements of Real\-Time Tasks with Time Redundancy”*\[[25](https://arxiv.org/html/2608.12762#bib.bib36)\]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:Letai​\(ki\)a\_\{i\}\(k\_\{i\}\)denote the additional processing time and runtime overhead required to toleratekik\_\{i\}faults during the mission time of a taskT~i\\tilde\{T\}\_\{i\}\. The worst\-case timing requirementWi​\(ki\)W\_\{i\}\(k\_\{i\}\)ofT~i\\tilde\{T\}\_\{i\}is given by

Wi​\(ki\)=Wi​\(0\)\+Ai​\(ki\),W\_\{i\}\(k\_\{i\}\)=W\_\{i\}\(0\)\+A\_\{i\}\(k\_\{i\}\),\(1\)whereAi​\(ki\)A\_\{i\}\(k\_\{i\}\)denotes the worst\-case value ofai​\(ki\)a\_\{i\}\(k\_\{i\}\)andWi​\(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\. LetR∗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\}\\cdot\(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](https://arxiv.org/html/2608.12762#A0.SS1.SSS1)\.

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\. SinceProsafollows an interpreted execution model inRocq, all prerequisite definitions and constructs must be available before they are referenced, making dependency\-aware ordering essential for correct compilation\.

### VI\-BRetrieval\-Augmented Generation

Given the informal sketch of an invariant, the next step is to translate it into aProsascript\. To support this translation, we employ retrieval\-augmented generation \(RAG\) over theProsacodebase\. We use the*statement*,*conclusion*, and*intuition*fields from the informal sketch as query, retrieve their independent results and keep the top\-kkresults from two complementary sources: \(i\)*example scripts*that demonstrate similar constructs or proof patterns, and \(ii\)*documentation fragments*describing the syntax, semantics, and usage conventions of relevantProsamodules\. Together, these provide the LLM with sufficient context to generate correct and idiomaticProsascript\.

### VI\-CSkeleton Code Generation

Using the retrieved context, we prompt the LLM to generate*skeleton code*—a structurally complete, type\-checkableProsascript in which all imports, section boundaries, type\-class contexts, variable declarations, and definition bodies are fully specified, while every proof obligation is replaced byAdmitted\.Listing[1](https://arxiv.org/html/2608.12762#LST1)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 viaAdmitted\.RequireExportprosa\.util\.all\.

RequireExportprosa\.behavior\.time\.

RequireExportprosa\.model\.task\.concept\.

RequireExportprosa\.model\.aggregate\.workload\.

SectionWorstCaseTimingRequirement\.

Context\{Task:TaskType\}\.

Context‘\{TaskCostTask\}\.

Context\{Job:JobType\}\.

Context‘\{JobTaskJobTask\}\.

Context‘\{JobCostJob\}\.

VariableW\_i\_0:work\.

Variablek\_i:nat\.

VariableR\_star:work\.

DefinitionW\_i\_k\_i\(A\_i\_k\_i:work\):work:=

W\_i\_0\+A\_i\_k\_i\.

LemmaW\_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\.

EndWorstCaseTimingRequirement\.

The skeleton faithfully encodes the structure of both invariants\. Definition 1 is realized as the functionW\_i\_k\_i, which takes the fault\-tolerance overheadA\_i\_k\_ias an argument and returns its sum with the failure\-free WCETW\_i\_0\. TheProsatypework, defined asnat, represents discrete units of processor service\. Claim 1 is stated asLemma W\_i\_k\_i\_retry, which asserts that instantiatingW\_i\_k\_iwith the retry\-specific overhead yields exactly Equation \([2](https://arxiv.org/html/2608.12762#S6.E2)\)\. The type\-class contexts \(TaskType,JobType,TaskCost, etc\.\) anchor the formalization withinProsa’s modeling framework and ensure that the definitions are compatible with the library’s broader infrastructure\.

TheAdmitted\.directive instructsRocqto 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\-DProof Completion

In the final phase, we prompt the LLM a second time to discharge theAdmittedobligations\. 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 specificAdmittedblock\. For this example, the LLM produces the following proof:

Listing 2:Completed proof of the retry\-based worst\-case timing requirementLemmaW\_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\.

unfoldW\_i\_k\_i\.

lia\.

Qed\.

The proof proceeds in two steps\. First,unfold W\_i\_k\_iδ\\delta\-reduces the definition, exposing the underlying goal:

W\_i\_0\+ki×\(R∗\+W\_i\_0\)=ki×\(R∗\+W\_i\_0\)\+W\_i\_0\.\\texttt\{W\\\_i\\\_0\}\+k\_\{i\}\\times\(R^\{\*\}\+\\texttt\{W\\\_i\\\_0\}\)=k\_\{i\}\\times\(R^\{\*\}\+\\texttt\{W\\\_i\\\_0\}\)\+\\texttt\{W\\\_i\\\_0\}\.This is an equality over natural numbers that follows directly from the commutativity of addition\. Theliatactic, which implements a decision procedure for linear integer arithmetic, discharges it automatically\. The completed script compiles underRocqand confirms that the retry\-based worst\-case timing requirement is a valid instantiation of the general fault\-tolerant WCET model formalized inProsa\.

This example demonstrates how our pipeline systematically transforms informal real\-time scheduling results into machine\-verifiedProsaproofs 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](https://arxiv.org/html/2608.12762#A0.SS6)\.

## VIIExperimental Setup

We evaluateProve\-RTby investigating the following research questions \(RQs\)\.

RQ1:To what extent canProve\-RTformalize schedulability tests asProsa/Rocqscripts?

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 ofProve\-RT?

### VII\-ASystem Invariant Dataset Construction

As one of the main artifacts of this work,Prove\-RTSystem Invariant Dataset is constructed, which is a large\-scale collection of schedulability\-analysis invariants designed to support and evaluate LLM\-assistedProsa/Rocqmechanization\. The dataset provides instances of the framework objects introduced earlier: schedulability analysesAA, extracted invariant setsII, informal sketchesKjK\_\{j\}, and dependency graphsGD=\(I,D\)G\_\{D\}=\(I,D\)\. Figure[4](https://arxiv.org/html/2608.12762#S7.F4)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](https://arxiv.org/html/2608.12762#A0.SS2)\.

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 usingSelenium\. ThenSeleniumwas 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 usingGROBID\. 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 ofProve\-RT\. In our implementation, we used Gemini\-2\.5\-Flash as the LLM and prompted it to identify candidate system invariantsIIfrom each schedulability analysis and to extract their summaries, informal sketchesKjK\_\{j\}, and dependency information for constructingGDG\_\{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 extractedidentifieranddependenciesfields, 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 exceeds0\.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 askeep,review, orreject: papers with dependency cycles or an unresolved\-dependency ratio above0\.150\.15are rejected, papers with weaker structural issues are marked for review, and structurally valid papers are retained\. After this filtering step, the retained corpus contained1,1911,191papers and13,13413,134informal 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 withRocq\-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 toRocqkeywords is provided in Appendix[\-H](https://arxiv.org/html/2608.12762#A0.SS8)\. Overall, the extraction process produced 13,134 normalized system invariants, including their dependency information\. Table[I](https://arxiv.org/html/2608.12762#S7.T1)reports the distribution of invariants across the normalized categories\.

![Refer to caption](https://arxiv.org/html/2608.12762v1/system_invariant_system_diagram.png)Fig\. 4:System Invariant Dataset CollectionWe 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 toProve\-RTand a reusable artifact for studying LLM\-assisted mechanization of real\-time systems schedulability analyses\. The distribution is described in Appendix[\-G](https://arxiv.org/html/2608.12762#A0.SS7)\.

### VII\-BBaselines

Prove\-RTis compared against direct LLM\-based generation ofProsa/Rocqscripts\. Since recent LLMs have shown strong capability in proof synthesis andRocqcode generation, and sinceProsais built on top ofRocq, these baselines evaluate whether LLMs can mechanize real\-time systems schedulability analyses without the additional guidance introduced byPROVE\-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 externalProsadocumentation 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\-CEvaluation Metrics

Prove\-RTcounts a generated script as successful only if it is accepted by theRocqproof 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 priorRocqproof\-generation work, where generated proofs are considered correct only when they lead the theorem prover to proof termination withQed\[[11](https://arxiv.org/html/2608.12762#bib.bib25),[39](https://arxiv.org/html/2608.12762#bib.bib31)\]\.

To measure the effectiveness ofProve\-RT, we usesuccess rate, a standard metric used in prior work to evaluateRocqcode and proof generation\[[44](https://arxiv.org/html/2608.12762#bib.bib32),[17](https://arxiv.org/html/2608.12762#bib.bib34),[15](https://arxiv.org/html/2608.12762#bib.bib33)\]\.

Success rate is measured as the fraction of proof constructs for which the tool generates a successful proof script:

Success Rate=NSNT,\\text\{Success Rate\}=\\frac\{N\_\{S\}\}\{N\_\{T\}\},\(3\)whereNSN\_\{S\}denotes the number of successfully mechanized sketches with successful proof scripts, andNTN\_\{T\}denotes the total number of evaluated sketches\.

### VII\-DImplementation Details

For the system invariant extraction stage,Gemini\-2\.5\-Flashwas 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 ofProsa, yielding5,0975,097documentation fragments from356356source files\. Three retrieval strategies were evaluated: BM25, dense retrieval, and hybrid retrieval\. For dense retrieval, thenomic\-embed\-code\-7bwas used to generate vector embeddings and store them in a FAISS vector index\. For each query, the top\-KKmost relevant documentation chunks were selected, withK=5K=5, and they were provided as context to the LLM during skeleton generation\.

The proof completion pipeline usesClaude\-Opus\-4\.6\. It is executed in two phases\. In the first phase, the skeleton code is synthesized withAdmitted\.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 runningRocqversion 9\.1\.0\.

TABLE I:Distribution of extracted elements by categoryThe 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 usingGROBIDto 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\.

## VIIIEvaluation

We evaluateProve\-RTaccording to the three research questions introduced in Section[VII](https://arxiv.org/html/2608.12762#S7)\.

Evaluation of RQ1\.To evaluate the effectiveness ofProve\-RT, we compare it against directProsa/Rocqscript generation using state\-of\-the\-art LLMs, including GPT and Claude\. Although these models have demonstrated strong general capabilities in generatingRocqcode, their ability to generateProsascripts 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 howProve\-RTguides these models for producing mechanically checkableProsa/Rocqscripts\.

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 existingProsaabstractions 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 contained109109papers and1,9041,904unit\-level informal sketches\.

From this curated evaluation corpus, we further selected a smaller evaluation subset of300300unit\-level informal sketches using proportional stratified sampling over dependency\-depth categories\. Letncn\_\{c\}denote the number of sketches in categorycc, and letNNdenote the total number of sketches in the curated corpus\. For each category, we computed the sampling quota as

qc=300⋅ncN\.q\_\{c\}=300\\cdot\\frac\{n\_\{c\}\}\{N\}\.We first selected⌊qc⌋\\lfloor q\_\{c\}\\rfloorsketches 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 of4242for reproducibility\.

TABLE II:Overall mechanization success across generation modes\.Prove\-RTachieves the best performance among the evaluated approaches when used with dense RAG, mechanizing134134informal sketches and achieving a success rate of44\.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 approximately32%32\\%and35%35\\%, respectively\[[39](https://arxiv.org/html/2608.12762#bib.bib31),[11](https://arxiv.org/html/2608.12762#bib.bib25)\]\. 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 thatProve\-RToperates in the specialized and low\-resource setting ofProsa\-based real\-time systems mechanization, a44\.7%44\.7\\%success rate indicates substantial progress\.

Other retrieval methods also perform competitively withinProve\-RT:BM25mechanizes126126sketches with a success rate of42\.0%42\.0\\%, while hybrid retrieval mechanizes123123sketches with a success rate of41\.0%41\.0\\%\. In contrast, direct generation with GPT fails to mechanize any construct, whether prompted with paper statements or informal sketches\. Claude mechanizes only11sketch from the informal sketches, corresponding to a success rate of0\.33%0\.33\\%\. These results suggest that direct prompting, even with structured informal sketches, is insufficient for reliableProsa/Rocqgeneration\. The detailed comparison is shown in Table[II](https://arxiv.org/html/2608.12762#S8.T2)\.

An interesting observation from the direct\-generation baselines is that both GPT and Claude often produce compilableRocqscripts without actually usingProsa\. In these cases, the generated scripts may type\-check inRocq, but they do not rely on the definitions, abstractions, or verified results provided by theProsalibrary\. Since our goal is to mechanize real\-time systems schedulability analyses withinProsa, we count such outputs as failures\.

In our study, Claude produced compilable scripts for3939of the300300informal sketches\. However, only11of these scripts usedProsa; the remaining3838were generic compilableRocqscripts and were therefore discarded\. The behavior was even more pronounced for GPT, it generated148148compilableRocqscripts out of300300attempts, but none of them usedProsa\. These results further highlight the limitation of direct LLM prompting, even when the generated output is syntactically valid and type\-correct inRocq, it may fail to mechanize the target schedulability analysis in the intendedProsaframework\.

This confirms that decomposing the task into sketch\-guided retrieval, skeleton generation, and proof completion improves the reliability of LLM\-assistedProsamechanization\.

Observation I\.Prove\-RTis substantially more effective than direct LLM prompting forProsa/Rocqmechanization\. On the300300sampled informal sketches,Prove\-RT\-denseachieves the best result, mechanizing134134sketches with a success rate of44\.7%44\.7\\%\. By contrast, direct generation with GPT\-5 produces no validProsamechanizations, and Claude\-Opus\-4\.6 succeeds on only11sketch \(0\.33%0\.33\\%\)\. This demonstrates that successful mechanization requires more than generalRocqgeneration ability; it requiresProsa\-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 most1010sections\. For each dependency depth, the blue bar shows the total number of sketches and the orange bar shows the number successfully formalized byProve\-RT\.Evaluation of RQ2\.To evaluate how the structural complexity of an informal sketch affects mechanization, we group the300300sampled 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 thatProve\-RTsuccessfully formalizes as compilableProsa/Rocqscripts\.

Figure[5](https://arxiv.org/html/2608.12762#S8.F5)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 byProve\-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 generatedProsa/Rocqcode depends on limited prior context\. In contrast, sketches with many sections requireProve\-RTto 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 thatProve\-RTcan 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 II\.The success ofProve\-RTdecreases as sketches contain more sections, suggesting that deeper dependency chains make mechanization harder\. Nevertheless,Prove\-RTsucceeds 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](https://arxiv.org/html/2608.12762#bib.bib31)\]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 inProve\-RTis different\. TheProsadocumentation 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\. InProve\-RT, retrieval queries are derived from the informal sketchKjK\_\{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 correspondingProsadocumentation 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 exactProsaidentifiers, theorem names, and library\-specific terminology\.

TABLE III:Effect of retrieval method onProve\-RT\.Table[III](https://arxiv.org/html/2608.12762#S8.T3)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 for134134out of300300sketches \(44\.7%44\.7\\%\)\. BM25 and Hybrid also perform competitively, proving126126and123123sketches, respectively\. At the section level, however, Hybrid compiles the largest number of individual sections, with608608compiled sections out of13931393\(43\.6%43\.6\\%\), slightly higher than Dense with597/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\.Table[IV](https://arxiv.org/html/2608.12762#S8.T4)further breaks down performance by target construct kind\. Dense retrieval performs best on definition sketches, proving125125out of278278cases \(45\.0%45\.0\\%\), suggesting that semantic retrieval is effective for matching informal descriptions toProsadefinitions\. However, for proof\-bearing constructs, the trend is different\. Combining lemmas and theorems, BM25 proves1212out of2222proof\-bearing sketches \(54\.5%54\.5\\%\), Hybrid proves1111out of2222\(50\.0%50\.0\\%\), and Dense proves99out of2222\(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 exactProsareferences 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 exactProsareferences\.

Observation III\.The choice of retrieval method affects both section\-level compilation and end\-to\-end mechanization\. Dense retrieval achieves the best overall result, fully mechanizing134/300134/300sketches \(44\.7%44\.7\\%\), while Hybrid compiles the most individual sections, with608/1393608/1393compiled 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\.

## IXConclusion

This paper introducedProve\-RT, an LLM\-assisted framework for generating mechanizedProsa/Rocqscripts for schedulability analyses in real\-time systems literature\.Prove\-RTcombines dependency\-aware informal sketch extraction, retrieval from processedProsadocumentation, staged skeleton generation, and proof completion to guide LLMs towardProsa\-aware mechanization\. Our evaluation shows that direct prompting of state\-of\-the\-art LLMs is insufficient for reliableProsageneration, whileProve\-RTachieves a success rate of44\.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 forProsa/Rocq\-based schedulability analysis are currently lacking and remain a major bottleneck for automated script generation\.

As a research prototype,Prove\-RTstill faces challenges with deeper dependency chains and proof\-bearing constructs that require preciseProsacontext\. 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 whichProve\-RTcan be used to mechanically verify the correctness of LLM\-generated schedulability results\.

## References

- \[1\]\(2023\)ProofNet: autoformalizing and formally proving undergraduate\-level mathematics\.External Links:2302\.12433,[Link](https://arxiv.org/abs/2302.12433)Cited by:[§II](https://arxiv.org/html/2608.12762#S2.p2.1)\.
- \[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\.InThirty\-sixth International Conference on Machine Learning \(ICML\),External Links:[Link](https://arxiv.org/abs/1904.03241)Cited by:[§II](https://arxiv.org/html/2608.12762#S2.p2.1)\.
- \[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\.,pp\.182–190\.External Links:[Document](https://dx.doi.org/10.1109/REAL.1990.128746)Cited by:[§\-F](https://arxiv.org/html/2608.12762#A0.SS6.7),[§\-F1](https://arxiv.org/html/2608.12762#A0.SS6.SSS1.p1.1)\.
- \[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\.In2022 IEEE Real\-Time Systems Symposium \(RTSS\),Vol\.,pp\.197–210\.External Links:[Document](https://dx.doi.org/10.1109/RTSS55097.2022.00026)Cited by:[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p2.1)\.
- \[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\.InProceedings of the 41st International Conference on Machine Learning,Proceedings of Machine Learning Research, Vol\.235,pp\.4046–4076\.External Links:[Link](https://proceedings.mlr.press/v235/blaauwbroek24a.html)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p5.1),[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p3.1)\.
- \[6\]L\. Blaauwbroek, J\. Urban, and H\. Geuvers\(2020\)The tactician: a seamless, interactive tactic learner and prover for coq\.InIntelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings,Berlin, Heidelberg,pp\.271–277\.External Links:ISBN 978\-3\-030\-53517\-9,[Link](https://doi.org/10.1007/978-3-030-53518-6_17),[Document](https://dx.doi.org/10.1007/978-3-030-53518-6%5F17)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p5.1),[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p3.1)\.
- \[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,pp\.03:1–03:2\.External Links:[Link](https://api.semanticscholar.org/CorpusID:220275236)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p4.1),[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p2.1)\.
- \[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](https://api.semanticscholar.org/CorpusID:9850815)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p2.1)\.
- \[9\]F\. Cerqueira, F\. Stutz, and B\. B\. Brandenburg\(2016\)PROSA: a case for readable mechanized schedulability analysis\.In2016 28th Euromicro Conference on Real\-Time Systems \(ECRTS\),Vol\.,pp\.273–284\.External Links:[Document](https://dx.doi.org/10.1109/ECRTS.2016.28)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p3.1),[§III\-A](https://arxiv.org/html/2608.12762#S3.SS1.p1.1),[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p2.1)\.
- \[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\),pp\.144–207\.External Links:ISSN 0922\-6443,[Link](https://doi.org/10.1007/s11241-018-9316-9),[Document](https://dx.doi.org/10.1007/s11241-018-9316-9)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p2.1)\.
- \[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\.InProceedings of the IEEE/ACM 47th International Conference on Software Engineering,ICSE ’25,pp\.29–41\.External Links:ISBN 9798331505691,[Link](https://doi.org/10.1109/ICSE55347.2025.00116),[Document](https://dx.doi.org/10.1109/ICSE55347.2025.00116)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p5.1),[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p3.1),[§VII\-C](https://arxiv.org/html/2608.12762#S7.SS3.p1.1),[§VIII](https://arxiv.org/html/2608.12762#S8.p5.1)\.
- \[12\]L\. de Moura, S\. Kong, J\. Avigad, F\. van Doorn, and J\. von Raumer\(2015\)The lean theorem prover \(system description\)\.InAutomated Deduction \- CADE\-25,A\. P\. Felty and A\. Middeldorp \(Eds\.\),Cham,pp\.378–388\.Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p5.1),[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p1.1)\.
- \[13\]R\. Devillers and J\. Goossens\(2000\)Liu and layland’s schedulability test revisited\.Inf\. Process\. Lett\.73\(5–6\),pp\.157–161\.External Links:ISSN 0020\-0190,[Link](https://doi.org/10.1016/S0020-0190(00)00016-8),[Document](https://dx.doi.org/10.1016/S0020-0190%2800%2900016-8)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p2.1)\.
- \[14\]E\. First, Y\. Brun, and A\. Guha\(2020\)TacTok: semantics\-aware proof synthesis\.4\(OOPSLA\)\.External Links:[Link](https://doi.org/10.1145/3428299),[Document](https://dx.doi.org/10.1145/3428299)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p5.1),[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p3.1)\.
- \[15\]E\. First, Y\. Brun, and A\. Guha\(2020\)TacTok: semantics\-aware proof synthesis\.4\(OOPSLA\)\.External Links:[Link](https://doi.org/10.1145/3428299),[Document](https://dx.doi.org/10.1145/3428299)Cited by:[§VII\-C](https://arxiv.org/html/2608.12762#S7.SS3.p2.1)\.
- \[16\]E\. First and Y\. Brun\(2022\)Diversity\-driven automated formal verification\.InProceedings of the 44th International Conference on Software Engineering,ICSE ’22,New York, NY, USA,pp\.749–761\.External Links:ISBN 9781450392211,[Link](https://doi.org/10.1145/3510003.3510138),[Document](https://dx.doi.org/10.1145/3510003.3510138)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p5.1),[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p3.1)\.
- \[17\]E\. First and Y\. Brun\(2022\)Diversity\-driven automated formal verification\.InProceedings of the 44th International Conference on Software Engineering,ICSE ’22,New York, NY, USA,pp\.749–761\.External Links:ISBN 9781450392211,[Link](https://doi.org/10.1145/3510003.3510138),[Document](https://dx.doi.org/10.1145/3510003.3510138)Cited by:[§VII\-C](https://arxiv.org/html/2608.12762#S7.SS3.p2.1)\.
- \[18\]P\. Fradet, X\. Guo, and S\. Quinton\(2023\)CertiCAN certifying can analyses and their results\.Real\-Time Syst\.59\(2\),pp\.160–198\.External Links:ISSN 0922\-6443,[Link](https://doi.org/10.1007/s11241-023-09393-2),[Document](https://dx.doi.org/10.1007/s11241-023-09393-2)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p4.1),[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p2.1)\.
- \[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](https://arxiv.org/abs/2602.22631)Cited by:[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p1.1)\.
- \[20\]X\. Guo, M\. Lesourd, M\. Liu, L\. Rieg, and Z\. Shao\(2019\)Integrating formal schedulability analysis into a verified os kernel\.InComputer Aided Verification,I\. Dillig and S\. Tasiran \(Eds\.\),Cham,pp\.496–514\.External Links:ISBN 978\-3\-030\-25543\-5Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p4.1)\.
- \[21\]J\. M\. Han, J\. Rute, Y\. Wu, E\. Ayers, and S\. Polu\(2022\)Proof artifact co\-training for theorem proving with language models\.InInternational Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=rpxJc9j04U)Cited by:[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p3.1)\.
- \[22\]A\. Q\. Jiang, W\. Li, J\. M\. Han, and Y\. Wu\(2021\)LISA: language models of ISAbelle proofs\.In6th Conference on Artificial Intelligence and Theorem Proving \(AITP\),Aussois, France,pp\.17:1–17:3\.External Links:[Link](https://aitp-conference.org/2021/abstract/paper_17.pdf)Cited by:[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p3.1)\.
- \[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\.InAdvances in Neural Information Processing Systems,Vol\.35,pp\.8360–8373\.External Links:[Link](https://proceedings.neurips.cc/paper_files/paper/2022/file/377c25312668e48f2e531e2f2c422483-Paper-Conference.pdf)Cited by:[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p3.1)\.
- \[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\.InProceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles,SOSP ’09,New York, NY, USA,pp\.207–220\.External Links:ISBN 9781605587523,[Link](https://doi.org/10.1145/1629575.1629596),[Document](https://dx.doi.org/10.1145/1629575.1629596)Cited by:[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p1.1)\.
- \[25\]H\. Lee, H\. Shin, and S\. Min\(1999\)Worst case timing requirement of real\-time tasks with time redundancy\.InProceedings Sixth International Conference on Real\-Time Computing Systems and Applications\. RTCSA’99 \(Cat\. No\.PR00306\),Vol\.,pp\.410–414\.External Links:[Document](https://dx.doi.org/10.1109/RTCSA.1999.811290)Cited by:[§VI\-A](https://arxiv.org/html/2608.12762#S6.SS1.p1.1)\.
- \[26\]X\. Leroy\(2009\)Formal verification of a realistic compiler\.Commun\. ACM52\(7\),pp\.107–115\.External Links:ISSN 0001\-0782,[Link](https://doi.org/10.1145/1538788.1538814),[Document](https://dx.doi.org/10.1145/1538788.1538814)Cited by:[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p1.1)\.
- \[27\]M\. Maida, S\. Bozhko, and B\. B\. Brandenburg\(2022\)Foundational Response\-Time Analysis as Explainable Evidence of Timeliness \(Artifact\)\.Dagstuhl Artifacts Series8\(1\),pp\.7:1–7:2\.Note:Keywords: hard real\-time systems, response\-time analysis, uniprocessor, Coq, Prosa, fixed priority, EDF, preemptive, non\-preemptive, verificationExternal Links:ISSN 2509\-8195,[Link](https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.1.7),[Document](https://dx.doi.org/10.4230/DARTS.8.1.7)Cited by:[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p2.1)\.
- \[28\]G\. Malecha, G\. Morrisett, A\. Shinnar, and R\. Wisnesky\(2010\)Toward a verified relational database management system\.InProceedings of the 37th Annual ACM SIGPLAN\-SIGACT Symposium on Principles of Programming Languages,POPL ’10,New York, NY, USA,pp\.237–248\.External Links:ISBN 9781605584799,[Link](https://doi.org/10.1145/1706299.1706329),[Document](https://dx.doi.org/10.1145/1706299.1706329)Cited by:[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p1.1)\.
- \[29\]G\. Nelissen, J\. Fonseca, G\. Raravi, and V\. Nélis\(2015\)Timing analysis of fixed priority self\-suspending sporadic tasks\.In2015 27th Euromicro Conference on Real\-Time Systems,Vol\.,pp\.80–89\.External Links:[Document](https://dx.doi.org/10.1109/ECRTS.2015.15)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p2.1)\.
- \[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 3540433767Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p5.1),[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p1.1)\.
- \[31\]S\. Polu and I\. Sutskever\(2020\)Generative language modeling for automated theorem proving\.ArXivabs/2009\.03393\.External Links:[Link](https://api.semanticscholar.org/CorpusID:221535103)Cited by:[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p3.1)\.
- \[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](https://arxiv.org/abs/2504.21801)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p5.1.4)\.
- \[33\]P\. Roux, S\. Quinton, and M\. Boyer\(2022\)A Formal Link Between Response Time Analysis and Network Calculus \(Artifact\)\.Dagstuhl Artifacts Series8\(1\),pp\.3:1–3:3\.Note:Keywords: Response Time Analysis, Network Calculus, dense time, discrete time, response time, formal proof, CoqExternal Links:ISSN 2509\-8195,[Link](https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.1.3),[Document](https://dx.doi.org/10.4230/DARTS.8.1.3)Cited by:[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p2.1)\.
- \[34\]A\. Sanchez\-Stern, Y\. Alhessi, L\. Saul, and S\. Lerner\(2020\)Generating correctness proofs with neural networks\.InProceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages,MAPL 2020,New York, NY, USA,pp\.1–10\.External Links:ISBN 9781450379960,[Link](https://doi.org/10.1145/3394450.3397466),[Document](https://dx.doi.org/10.1145/3394450.3397466)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p5.1),[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p3.1)\.
- \[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](https://doi.org/10.1145/3593374),[Document](https://dx.doi.org/10.1145/3593374)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p5.1),[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p3.1)\.
- \[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](https://arxiv.org/abs/2505.20613)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p5.1.4)\.
- \[37\]\(2019\)The lean mathematical library\.CoRRabs/1910\.09336\.External Links:[Link](http://arxiv.org/abs/1910.09336),1910\.09336Cited by:[§II](https://arxiv.org/html/2608.12762#S2.p2.1)\.
- \[38\]\(2026\)The rocq prover\.Note:Available at[https://rocq\-prover\.org/doc/V9\.2\.0/refman/index\.html](https://rocq-prover.org/doc/V9.2.0/refman/index.html)\. Last accessed: 2026\-05\-21Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p3.1),[§I](https://arxiv.org/html/2608.12762#S1.p5.1),[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p1.1)\.
- \[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\.InProceedings of the IEEE/ACM 47th International Conference on Software Engineering,ICSE ’25,pp\.347–359\.External Links:ISBN 9798331505691,[Link](https://doi.org/10.1109/ICSE55347.2025.00161),[Document](https://dx.doi.org/10.1109/ICSE55347.2025.00161)Cited by:[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p3.1),[§VII\-C](https://arxiv.org/html/2608.12762#S7.SS3.p1.1),[§VIII](https://arxiv.org/html/2608.12762#S8.p16.1),[§VIII](https://arxiv.org/html/2608.12762#S8.p5.1)\.
- \[40\]\(2007\)Towards a practical programming language based on dependent type theory\.External Links:[Link](https://api.semanticscholar.org/CorpusID:118357515)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p5.1),[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p1.1)\.
- \[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](https://arxiv.org/abs/2407.11214)Cited by:[§II](https://arxiv.org/html/2608.12762#S2.p2.1)\.
- \[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\.InProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation,PLDI ’15,New York, NY, USA,pp\.357–368\.External Links:ISBN 9781450334686,[Link](https://doi.org/10.1145/2737924.2737958),[Document](https://dx.doi.org/10.1145/2737924.2737958)Cited by:[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p1.1)\.
- \[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](https://arxiv.org/abs/2502.03438)Cited by:[§I](https://arxiv.org/html/2608.12762#S1.p5.1.4)\.
- \[44\]K\. Yang and J\. Deng\(2019\)Learning to prove theorems via interacting with proof assistants\.CoRRabs/1905\.09381\.External Links:[Link](http://arxiv.org/abs/1905.09381),1905\.09381Cited by:[§II](https://arxiv.org/html/2608.12762#S2.p2.1),[§VII\-C](https://arxiv.org/html/2608.12762#S7.SS3.p2.1)\.
- \[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\.InAdvances in Neural Information Processing Systems,Vol\.36,pp\.21573–21612\.External Links:[Link](https://proceedings.neurips.cc/paper_files/paper/2023/file/4441469427094f8873d0fecb0c4e1cee-Paper-Datasets_and_Benchmarks.pdf)Cited by:[§III\-B](https://arxiv.org/html/2608.12762#S3.SS2.p3.1)\.
- \[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:[§II](https://arxiv.org/html/2608.12762#S2.p2.1)\.

### \-AIllustrative Example withWorst\-Case Timing Requirements of Real\-Time Tasks with Time Redundancy

#### \-A1Extracted JSON and Informal Sketch for Illustrative Example

Listing[3](https://arxiv.org/html/2608.12762#LST3)presents the extracted json that is used for the Section[VI](https://arxiv.org/html/2608.12762#S6)\.

Listing 3:Structured extraction of Definition 1 and Claim 1\[

\{

"type":"definition",

"identifier":"Definition1",

"formal\_description":\{

"statement":"W\_i\_k\_i=W\_i\_0\+A\_i\_k\_i",

"variables":\{

"W\_i\_k\_i":"Worstcasetimingrequirementoftask

tau\_iinthepresenceofk\_ifaults",

"W\_i\_0":"Failure\-freecomputationalrequirement

\(WCET\)oftasktau\_i",

"A\_i\_k\_i":"Worstcasevalueofadditional

reprocessingtimeandoverheadto

toleratek\_ifaults"

\},

"assumptions":\[

"Faultsaretransientorintermittent",

"Faultsaredetectedimmediatelyuponoccurrence"

\],

"conclusion":"Definesthetotaltimeataskrequires

tocompleteitsexecutionandrecovery

actions\."

\},

"informal\_sketch":\{

"intuition":"Thetotaltimeataskneedsisits

normalexecutiontimeplusthemaximum

possibletimespentonfaultdetection,

recovery,andre\-execution\.",

"steps":\[

"Identifythebaseexecutiontimewithoutfaults

W\_i\_0",

"CalculatethemaximumoverheadA\_i\_k\_ibasedon

thespecificredundancytechniqueused",

"Sumthemtofindthetotaltimingrequirement"

\],

"key\_insights":\[

"Separatesthefunctionalexecutiontimefromthe

fault\-toleranceoverhead"

\]

\},

"dependencies":\[\]

\},

\{

"type":"claim",

"identifier":"Claim1",

"formal\_description":\{

"statement":"W\_i\_k\_i=k\_i\*\(R\_star\+W\_i\_0\)

\+W\_i\_0",

"variables":\{

"W\_i\_k\_i":"Worstcasetimingrequirementfor

retry",

"k\_i":"Numberoffaults",

"R\_star":"Taskrestartoverhead\(constant\)",

"W\_i\_0":"Failure\-freeWCET"

\},

"assumptions":\[

"Taskmustrestartfromtheverybeginningafter

everyfault"

\],

"conclusion":"CalculatestheWCTRfortheRetry

redundancytechnique\."

\},

"informal\_sketch":\{

"intuition":"Ifafaultoccurs,thetasklosesall

progressandmustrestart\.Intheworst

case,afaultoccursjustbefore

completion,requiringafullre\-execution

plusrestartoverheadforeveryfault\.",

"steps":\[

"Foreachofthek\_ifaults,addthecostofa

fullrestart\(R\_star\)andafullre\-execution

\(W\_i\_0\)",

"Addthefinalsuccessfulexecutiontime\(W\_i\_0\)"

\],

"key\_insights":\[

"Retryisthemostexpensivetechniquebecauseit

discardsallworkdonepriortothefault"

\]

\},

"dependencies":\["Definition1"\]

\}

\]

Listing[4](https://arxiv.org/html/2608.12762#LST4)presents the informal sketch that is used for the Section[VI](https://arxiv.org/html/2608.12762#S6)\. This sketch is formatted as structuredRocqcomments and serves as the direct input to the skeleton code generation phase\.

Listing 4:Informal sketch used as input to skeleton code generation====section====

definitionDefinition1

Statement:

W\_i\_k\_i=W\_i\_0\+A\_i\_k\_i

Variables:

W\_i\_k\_i:Worstcasetimingrequirementoftask

tau\_iinthepresenceofk\_ifaults

W\_i\_0:Failure\-freecomputationalrequirement

\(WCET\)oftasktau\_i

A\_i\_k\_i:Worstcasevalueofadditional

reprocessingtimeandoverheadto

toleratek\_ifaults

Assumptions:

1\.Faultsaretransientorintermittent

2\.Faultsaredetectedimmediatelyuponoccurrence

Conclusion:

Definesthetotaltimeataskrequirestocomplete

itsexecutionandrecoveryactions\.

Intuitionforgeneratingcode:

Thetotaltimeataskneedsisitsnormalexecution

timeplusthemaximumpossibletimespentonfault

detection,recovery,andre\-execution\.

Stepsforgeneratingcode:

1\.Identifythebaseexecutiontimewithoutfaults

W\_i\_0

2\.CalculatethemaximumoverheadA\_i\_k\_ibasedon

thespecificredundancytechniqueused

3\.Sumthemtofindthetotaltimingrequirement

KeyInsights:

1\.Separatesthefunctionalexecutiontimefromthe

fault\-toleranceoverhead

\*\)

====section====

claimClaim1

Statement:

W\_i\_k\_i=k\_i\*\(R\_star\+W\_i\_0\)\+W\_i\_0

Variables:

W\_i\_k\_i:Worstcasetimingrequirementforretry

k\_i:Numberoffaults

R\_star:Taskrestartoverhead\(constant\)

W\_i\_0:Failure\-freeWCET

Assumptions:

1\.Taskmustrestartfromtheverybeginningafter

everyfault

Conclusion:

CalculatestheWCTRfortheRetryredundancy

technique\.

Intuitionforgeneratingcode:

Ifafaultoccurs,thetasklosesallprogressand

mustrestart\.Intheworstcase,afaultoccurs

justbeforecompletion,requiringafull

re\-executionplusrestartoverheadforeveryfault\.

Stepsforgeneratingcode:

1\.Foreachofthek\_ifaults,addthecostofa

fullrestart\(R\_star\)andafullre\-execution

\(W\_i\_0\)

2\.Addthefinalsuccessfulexecutiontime\(W\_i\_0\)

KeyInsights:

1\.Retryisthemostexpensivetechniquebecauseit

discardsallworkdonepriortothefault

\*\)

### \-BIEEE 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"\),

### \-CProsa Documentation Details

TABLE V:Role of majorProsadocumentation modules\.
### \-DPseudocode for skeleton code generation

The pseudocode is presented in Algorithm[1](https://arxiv.org/html/2608.12762#alg1)

Algorithm 1Phase 1: Skeleton Code Generation1:Sketch sections

𝒮\\mathcal\{S\}, retry budget

MsM\_\{s\}
2:Skeleton script

PP
3:

P←∅P\\leftarrow\\emptyset⊳\\trianglerightaccumulated script

4:foreach section

si∈𝒮s\_\{i\}\\in\\mathcal\{S\}do

5:

Ci←RetrieveContext​\(si\)C\_\{i\}\\leftarrow\\textsc\{RetrieveContext\}\(s\_\{i\}\)
6:

ki←InferKind​\(si\)k\_\{i\}\\leftarrow\\textsc\{InferKind\}\(s\_\{i\}\)
7:

s​u​c​c​e​s​s←f​a​l​s​esuccess\\leftarrow false
8:for

a←1a\\leftarrow 1to

MsM\_\{s\}do

9:

πi←BuildPrompt​\(si,Ci,P,ki\)\\pi\_\{i\}\\leftarrow\\textsc\{BuildPrompt\}\(s\_\{i\},C\_\{i\},P,k\_\{i\}\)
10:

bi←GenerateBlock​\(πi\)b\_\{i\}\\leftarrow\\textsc\{GenerateBlock\}\(\\pi\_\{i\}\)
11:

bi←Normalize​\(bi\)b\_\{i\}\\leftarrow\\textsc\{Normalize\}\(b\_\{i\}\)
12:if

¬CheckSkeletonRules​\(bi\)\\neg\\textsc\{CheckSkeletonRules\}\(b\_\{i\}\)then

13:continue

14:endif

15:if

¬CheckAssumptions​\(bi,si\)\\neg\\textsc\{CheckAssumptions\}\(b\_\{i\},s\_\{i\}\)then

16:continue

17:endif

18:

P′←Concat​\(P,bi\)P^\{\\prime\}\\leftarrow\\textsc\{Concat\}\(P,b\_\{i\}\)
19:if

Compile​\(P′\)\\textsc\{Compile\}\(P^\{\\prime\}\)then

20:

P←P′P\\leftarrow P^\{\\prime\}
21:

UpdateContext​\(P,bi\)\\textsc\{UpdateContext\}\(P,b\_\{i\}\)
22:

s​u​c​c​e​s​s←t​r​u​esuccess\\leftarrow true
23:break

24:endif

25:endfor

26:if

s​u​c​c​e​s​s=f​a​l​s​esuccess=falsethen

27:return

Failure​\(si\)\\textsc\{Failure\}\(s\_\{i\}\)
28:endif

29:endfor

30:return

PP

### \-EPseudocode for Batch Completion with Iterative Repair

The pseudocode is presented in Algorithm[2](https://arxiv.org/html/2608.12762#alg2)

Algorithm 2Phase 2a: Batch Completion with Compiler\-Guided Repair1:Skeleton sections

ℬ\\mathcal\{B\}, retry budget

MbM\_\{b\}
2:Completed script

PP
3:

P←∅P\\leftarrow\\emptyset⊳\\trianglerightcompleted script

4:foreach section

Bi∈ℬB\_\{i\}\\in\\mathcal\{B\}do

5:if

¬HasAdmitted​\(Bi\)\\neg\\textsc\{HasAdmitted\}\(B\_\{i\}\)then

6:

P←Concat​\(P,Bi\)P\\leftarrow\\textsc\{Concat\}\(P,B\_\{i\}\)
7:continue

8:endif

9:

Ci←RetrieveContext​\(Bi\)C\_\{i\}\\leftarrow\\textsc\{RetrieveContext\}\(B\_\{i\}\)
10:

πi←BuildCompletionPrompt​\(Bi,Ci,P\)\\pi\_\{i\}\\leftarrow\\textsc\{BuildCompletionPrompt\}\(B\_\{i\},C\_\{i\},P\)
11:

pi←GenerateProof​\(πi\)p\_\{i\}\\leftarrow\\textsc\{GenerateProof\}\(\\pi\_\{i\}\)
12:

Bi′←ReplaceAdmitted​\(Bi,pi\)B\_\{i\}^\{\\prime\}\\leftarrow\\textsc\{ReplaceAdmitted\}\(B\_\{i\},p\_\{i\}\)
13:

P′←Concat​\(P,Bi′\)P^\{\\prime\}\\leftarrow\\textsc\{Concat\}\(P,B\_\{i\}^\{\\prime\}\)
14:

s​u​c​c​e​s​s←Compile​\(P′\)success\\leftarrow\\textsc\{Compile\}\(P^\{\\prime\}\)
15:for

a←1a\\leftarrow 1to

MbM\_\{b\}do

16:if

s​u​c​c​e​s​ssuccessthen

17:break

18:endif

19:

ei←ExtractError​\(P′\)e\_\{i\}\\leftarrow\\textsc\{ExtractError\}\(P^\{\\prime\}\)
20:

ρi←BuildRepairPrompt​\(Bi′,Ci,ei\)\\rho\_\{i\}\\leftarrow\\textsc\{BuildRepairPrompt\}\(B\_\{i\}^\{\\prime\},C\_\{i\},e\_\{i\}\)
21:

pi←RepairProof​\(ρi\)p\_\{i\}\\leftarrow\\textsc\{RepairProof\}\(\\rho\_\{i\}\)
22:

Bi′←ApplyRepair​\(Bi′,pi\)B\_\{i\}^\{\\prime\}\\leftarrow\\textsc\{ApplyRepair\}\(B\_\{i\}^\{\\prime\},p\_\{i\}\)
23:

P′←Concat​\(P,Bi′\)P^\{\\prime\}\\leftarrow\\textsc\{Concat\}\(P,B\_\{i\}^\{\\prime\}\)
24:

s​u​c​c​e​s​s←Compile​\(P′\)success\\leftarrow\\textsc\{Compile\}\(P^\{\\prime\}\)
25:endfor

26:if

s​u​c​c​e​s​ssuccessthen

27:

P←P′P\\leftarrow P^\{\\prime\}
28:

MarkCompleted​\(Bi′\)\\textsc\{MarkCompleted\}\(B\_\{i\}^\{\\prime\}\)
29:else

30:

P←Concat​\(P,Bi\)P\\leftarrow\\textsc\{Concat\}\(P,B\_\{i\}\)
31:

MarkFailed​\(Bi\)\\textsc\{MarkFailed\}\(B\_\{i\}\)
32:endif

33:endfor

34:return

PP

### \-FIllustrative Example with*“Preemptively Scheduling Hard\-Real\-Time Sporadic Tasks on One Processor”*\[[3](https://arxiv.org/html/2608.12762#bib.bib35)\]

We illustrate another workflow ofProve\-RTusing a concrete schedulability analysis drawn from the RTS literature, starting with the extraction of intermediate representations and leading to the final machine\-verifiedProsascript\.

#### \-F1Source Material and Extraction

We consider the paper*“Preemptively Scheduling Hard\-Real\-Time Sporadic Tasks on One Processor”*\[[3](https://arxiv.org/html/2608.12762#bib.bib35)\]as a representative example\. From this paper, we extract the following definitions and lemma\. In particular, the lemmaOptimality 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\}\),whereeie\_\{i\}is the execution time,did\_\{i\}the relative deadline, andpip\_\{i\}the minimum separation between consecutive requests, withei≤die\_\{i\}\\leq d\_\{i\}andei≤pie\_\{i\}\\leq p\_\{i\}\. A task system is a finite setτ=\{T1,…,Tn\}\\tau=\\\{T\_\{1\},\\ldots,T\_\{n\}\\\}\.

Definition 2 \(Request Model\)\.A request of taskTiT\_\{i\}released at timet0t\_\{0\}is represented as\(i,t0\)\(i,t\_\{0\}\)\. It requireseie\_\{i\}units of processor time in the interval

\[t0,t0\+di\),\[t\_\{0\},t\_\{0\}\+d\_\{i\}\),so its absolute deadline ist0\+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 leastpip\_\{i\}:

\|t1−t2\|≥pi\.\|t\_\{1\}\-t\_\{2\}\|\\geq 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 timettif

t0≤t<t0\+dit\_\{0\}\\leq t<t\_\{0\}\+d\_\{i\}and it has not yet receivedeie\_\{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\.\\tau\\text\{ is feasible\}\\iff\\begin\{aligned\} &\\text\{the deadline algorithm succeeds\}\\\\ &\\text\{for every legal request set\}\.\\end\{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](https://arxiv.org/html/2608.12762#LST5)was extracted for this proof construct

Listing 5:Extracted Informal Sketch for Optimality of the Deadline Algorithm\.====section====

definitionDefinition1

Statement:

Asporadictasktask\_iisatripletask\_i=e\_i,d\_i,p\_iwheree\_i,d\_i,andp\_iarepositiveintegers,e\_i<=d\_i,ande\_i<=p\_i\.Asporadictasksystemtask\_systemisafinitesettask\_system=task\_1,task\_2,\.\.\.,task\_n\.

Variables:

task\_i:sporadictaski

task\_system:setofsporadictasks

e\_i:executiontimeoftask\_i

d\_i:relativedeadlineoftask\_i

p\_i:minimumseparationbetweensuccessiverequestsoftask\_i

n:numberoftasks

Assumptions:

1\.singleprocessor

2\.preemptivescheduling

3\.discretetimemodel

4\.e\_i,d\_i,p\_iarepositiveintegers

5\.e\_i<=d\_i

6\.e\_i<=p\_i

Conclusion:

Definesthesporadictaskmodelandthetask\-systemmodel\.

Intuitionforgeneratingcode:

Eachsporadictaskcanreleasejobsatarbitrarytimes,butnottoofrequently\.Theparameterp\_ipreventsinfinitelydensereleases,whilee\_iandd\_idescribehowmuchprocessortimeeachreleasedjobneedsandwhenitmustcomplete\.

Stepsforgeneratingcode:

1\.Representeachtasktask\_ibyexecutiontimee\_i,deadlined\_i,andminimumseparationp\_i\.

2\.Requiree\_i<=d\_isothateachindividualjobcanfitinsideitsowndeadlinewindow\.

3\.Requiree\_i<=p\_isothatthetaskdoesnotrequestmoreexecutionthanitsminimuminter\-arrivalspacingcanplausiblysupport\.

4\.Collectalltasksintotask\_system\.

KeyInsights:

1\.Theminimumseparationp\_iisthekeydistinctionbetweensporadicandarbitraryaperiodicarrivals\.

2\.Themodelallowsd\_i\>p\_i,sojobsofthesametaskmayhaveoverlappingdeadlinewindows\.

\*\)

====section====

definitionDefinition2

Statement:

LetP=lcm\(p\_1,p\_2,\.\.\.,p\_n\)\.Arequestoftask\_iattimet\_0isrepresentedbyrequest\_i\_t\_0=i,t\_0\.Therequestrequirese\_iunitsofprocessorallocationininterval\[t\_0,t\_0\+d\_i\)\.

Variables:

P:leastcommonmultipleofallminimumseparationsp\_i

request\_i\_t\_0:requestoftask\_ireleasedattimet\_0

t\_0:releasetimeofarequest

e\_i:executionrequirementoftask\_i

d\_i:relativedeadlineoftask\_i

p\_i:minimumseparationoftask\_i

Assumptions:

1\.task\_ibelongstotask\_system

2\.t\_0\>=0

3\.timeisdiscrete

Conclusion:

Definestaskrequestsandtheirexecutionwindows\.

Intuitionforgeneratingcode:

Asporadictaskgeneratesindividualrequestsorjobs\.Arequestreleasedatt\_0mustreceivee\_iunitsofservicebeforeitsabsolutedeadlinet\_0\+d\_i\.

Stepsforgeneratingcode:

1\.Takeatasktask\_iandreleasetimet\_0\.

2\.Constructrequest\_i\_t\_0\.

3\.Settheabsolutedeadlinetot\_0\+d\_i\.

4\.Requiretheschedulertoallocatee\_itimeunitsinside\[t\_0,t\_0\+d\_i\)\.

KeyInsights:

1\.Schedulabilityischeckedoverrequests,notjustovertaskparameters\.

2\.Theabsolutedeadlineisrelease\_timeplusrelativedeadline\.

\*\)

====section====

definitionDefinition3

Statement:

Asetofrequestsrequest\_setisschedulableiffthereexistsaprocessorschedulethatallocatese\_itimeunitstoeveryrequestrequest\_i\_t\_0inrequest\_setwithin\[t\_0,t\_0\+d\_i\)\.Asetrequest\_setislegaliffforanytworequestsrequest\_i\_t\_1andrequest\_i\_t\_2ofthesametask,abs\(t\_1\-t\_2\)\>=p\_i\.Thetask\_systemisfeasibleiffeverylegalrequest\_setisschedulable\.

Variables:

request\_set:setoftaskrequests

request\_i\_t\_0:requestoftask\_ireleasedatt\_0

t\_1:releasetimeofonerequest

t\_2:releasetimeofanotherrequest

p\_i:minimumseparationoftask\_i

task\_system:sporadictasksystem

Assumptions:

1\.singleprocessor

2\.preemptivescheduling

3\.allrequestssatisfytheirtaskparameters

Conclusion:

Definesschedulabilityofarequestset,legalityofarrivals,andfeasibilityofasporadictasksystem\.

Intuitionforgeneratingcode:

Arequestsetislegalifitrespectsthesporadicseparationconstraints\.Atasksystemisfeasibleonlyifeverypossiblelegalarrivalpatterncanbescheduledwithoutmissingdeadlines\.

Stepsforgeneratingcode:

1\.Checkallpairsofrequestsofthesametask\.

2\.Ifanytworeleasesarecloserthanp\_i,therequestsetisillegal\.

3\.Iftherequestsetislegal,askwhetheravalidpreemptivesingle\-processorscheduleexists\.

4\.Thetasksystemisfeasibleonlywheneverylegalrequestsethassuchaschedule\.

KeyInsights:

1\.Feasibilityisauniversalpropertyoveralllegalarrivalsequences\.

2\.Thedifficultycomesfromtheunboundednumberofpossiblelegalsporadicrequestsets\.

\*\)

====section====

definitionDefinition4

Statement:

AnonlineschedulingalgorithmUmapseachrequest\_setandtimettoeitheraselectedactiverequestrequest\_i\_t\_0,anidledecision,andoptionallyfailure\.Arequestrequest\_i\_t\_0isactiveattimetifft\_0<=t<t\_0\+d\_iandtherequesthasnotyetreceivede\_iunitsofprocessorallocationin\[t\_0,t\)\.Ureportsfailureattimetiffthereexistsrequest\_i\_t\_0suchthatt\_0\+d\_i=tandtherequesthasreceivedlessthane\_iunitsin\[t\_0,t\)\.

Variables:

U:onlineschedulingalgorithm

request\_set:setofrequestspresentedtoU

t:currenttime

request\_i\_t\_0:requestoftask\_ireleasedatt\_0

active:predicateindicatingthatarequestispendingandbeforeitsdeadline

failure:eventindicatingamisseddeadline

Assumptions:

1\.requestsarepresentedtoUattheirreleasetimes

2\.Uisonlineanditerative

3\.preemptionisallowedatintegertimeboundaries

Conclusion:

Definesonlinescheduling,activerequests,andfailure\.

Intuitionforgeneratingcode:

Ateachtime,theschedulereitherrunsoneactiverequestoridles\.Failureoccursexactlywhenarequestreachesitsdeadlinewithouthavingreceivedenoughexecution\.

Stepsforgeneratingcode:

1\.Ateachtimet,identifyallactiverequests\.

2\.Chooseoneactiverequesttoexecuteorleavetheprocessoridle\.

3\.Updatetheamountofservicereceivedbythechosenrequest\.

4\.Ifanyrequestreachesitsdeadlinewithoutreceivinge\_iservice,reportfailure\.

KeyInsights:

1\.Failureisdefinedatthedeadlineboundary\.

2\.Theactive\-requestdefinitioncapturesunfinishedjobsthatarestilleligibletoexecute\.

\*\)

====section====

definitionDefinition5

Statement:

ThedeadlinealgorithmUallocatestheprocessorattimettotheactiverequestwiththenearestabsolutedeadline\.Foractiverequestsrequest\_i\_t\_1andrequest\_j\_t\_2,Uchoosesrequest\_i\_t\_1overrequest\_j\_t\_2ift\_1\+d\_i<t\_2\+d\_j,orift\_1\+d\_i=t\_2\+d\_jandi<j\.

Variables:

U:deadlinealgorithm

request\_i\_t\_1:activerequestoftask\_ireleasedatt\_1

request\_j\_t\_2:activerequestoftask\_jreleasedatt\_2

t\_1\_plus\_d\_i:absolutedeadlineofrequest\_i\_t\_1

t\_2\_plus\_d\_j:absolutedeadlineofrequest\_j\_t\_2

Assumptions:

1\.preemptivescheduling

2\.singleprocessor

3\.tiesarebrokenbylowertaskindex

Conclusion:

Definesthedeadline\-drivenschedulingalgorithmusedthroughoutthepaper\.

Intuitionforgeneratingcode:

Thedeadlinealgorithmisearliest\-deadline\-firstwithadeterministictie\-breakingrule\.Therequestwhosedeadlineisclosestgetstheprocessor\.

Stepsforgeneratingcode:

1\.Attimet,collectallactiverequests\.

2\.Computeeachactiverequest’sabsolutedeadline\.

3\.Selecttherequestwiththesmallestabsolutedeadline\.

4\.Iftworequestshavethesameabsolutedeadline,choosetheonewithsmallertaskindex\.

KeyInsights:

1\.ThealgorithmisEDFspecializedtothepaper’srequestmodel\.

2\.Tie\-breakingdoesnotaffectwhetherfailureoccurs,butmakesthescheduledeterministic\.

\*\)

====section====

lemmaLemma1

Statement:

Thedeadline\_algorithm\_Uisoptimalforsporadictasksystems\.Givenanyrequest\_set,Uconstructsascheduleforrequest\_setifoneexists;otherwiseUreportsfailureatsometime\.Thereforetask\_systemisfeasibleiffUconstructsascheduleforeverylegalrequest\_set\.

Variables:

deadline\_algorithm\_U:earliest\-deadlineschedulingalgorithm

request\_set:setofrequests

task\_system:sporadictasksystem

Assumptions:

1\.singleprocessor

2\.preemptivescheduling

3\.sporadicrequestmodel

4\.legalrequestsetsrespectminimumseparations

Conclusion:

EDF\-styledeadlineschedulingissufficienttodecidefeasibilityoverlegalrequestsets\.

Intuitionforgeneratingcode:

Forpreemptiveuniprocessorscheduling,alwaysrunningtheactivejobwiththeearliestdeadlineisoptimal:ifanyschedulecanmeetalldeadlines,thedeadlinealgorithmcanalsomeetthem\.

Stepsforgeneratingcode:

1\.Consideranylegalrequestset\.

2\.Runthedeadlinealgorithmonthatrequestset\.

3\.Ifanyfeasiblescheduleexists,thedeadlinealgorithmalsosucceeds\.

4\.Ifthedeadlinealgorithmfails,nofeasiblescheduleexistsforthatrequestset\.

5\.Thustask\_systemisfeasibleexactlywhenthedeadlinealgorithmneverfailsonanylegalrequestset\.

KeyInsights:

1\.Thislemmaletsthepaperfocusononecanonicalschedulerratherthanallpossibleschedules\.

2\.Itconvertsfeasibilityintoabsenceoffailureunderthedeadlinealgorithm\.

\*\)

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\. SinceProsa/Rocqrequires all referenced constructs to be defined before use, dependency\-aware ordering is necessary for successful compilation\.

#### \-F2Retrieval\-Augmented Generation

Given the informal sketch of an invariant, the next step is to translate it into aProsascript\. To support this translation, we employ retrieval\-augmented generation \(RAG\) over theProsacodebase\. We use the*statement*,*conclusion*, and*intuition*fields from the informal sketch as a joint query and retrieve the top\-kkresults from two complementary sources: \(i\)*example scripts*that demonstrate similar constructs or proof patterns, and \(ii\)*documentation fragments*describing the syntax, semantics, and usage conventions of relevantProsamodules\. Together, these provide the LLM with sufficient context to generate correct and idiomatic code\.

#### \-F3Skeleton Code Generation

Using the retrieved context, we prompt the LLM to generate*skeleton code*—a structurally complete, type\-checkableProsascript in which all imports, section boundaries, type\-class contexts, variable declarations, and definition bodies are fully specified, while every proof obligation is replaced byAdmitted\.Listing[6](https://arxiv.org/html/2608.12762#LST6)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 viaAdmitted\.FrommathcompRequireImportall\_ssreflect\.

RequireImportprosa\.model\.task\.concept\.

RequireImportprosa\.model\.task\.arrival\.sporadic\.

RequireImportprosa\.model\.priority\.edf\.

RequireImportprosa\.model\.processor\.ideal\.

RequireImportprosa\.model\.readiness\.basic\.

RequireImportprosa\.analysis\.definitions\.schedulability\.

RequireImportprosa\.analysis\.facts\.behavior\.completion\.

RequireExportprosa\.results\.edf\.optimality\.

SectionSporadicEDFOptimality\.

Context\{Task:TaskType\}‘\{TaskCostTask\}‘\{TaskDeadlineTask\}‘\{SporadicModelTask\}\.

Context\{Job:JobType\}‘\{JobTaskJobTask\}‘\{JobArrivalJob\}‘\{JobCostJob\}‘\{JobDeadlineJob\}\.

Variablets:seqTask\.

HypothesisH\_job\_deadline\_def:

forallj,job\_deadlinej=job\_arrivalj\+task\_deadline\(job\_taskj\)\.

Definitionvalid\_sporadic\_task\(tsk:Task\):Prop:=

\[/\\0<task\_costtsk,

0<task\_deadlinetsk,

0<task\_min\_inter\_arrival\_timetsk,

task\_costtsk<=task\_deadlinetsk&

task\_costtsk<=task\_min\_inter\_arrival\_timetsk\]\.

Definitionrequest\_absolute\_deadline\(j:Job\):instant:=

job\_arrivalj\+task\_deadline\(job\_taskj\)\.

Definitionfeasible:Prop:=

forallarr\_seq:arrival\_sequenceJob,

valid\_arrival\_sequencearr\_seq\-\>

\(foralltsk,tsk\\ints\-\>respects\_sporadic\_task\_modelarr\_seqtsk\)\-\>

existssched:schedule\(ideal\.processor\_stateJob\),

valid\_scheduleschedarr\_seq/\\all\_deadlines\_of\_arrivals\_metarr\_seqsched\.

Definitiononline\_failure\_at

\(arr\_seq:arrival\_sequenceJob\)

\(sched:schedule\(ideal\.processor\_stateJob\)\)\(t:instant\):Prop:=

existsj,arrives\_inarr\_seqj/\\job\_deadlinej=t/\\~~completed\_byschedjt\.

Definitiondeadline\_algorithm\_U\(sched:schedule\(ideal\.processor\_stateJob\)\):Prop:=

EDF\_schedulesched\.

Lemmadeadline\_algorithm\_optimal:

feasible<\-\>

\(forallarr\_seq:arrival\_sequenceJob,

valid\_arrival\_sequencearr\_seq\-\>

\(foralltsk,tsk\\ints\-\>respects\_sporadic\_task\_modelarr\_seqtsk\)\-\>

existssched:schedule\(ideal\.processor\_stateJob\),

valid\_scheduleschedarr\_seq/\\

all\_deadlines\_of\_arrivals\_metarr\_seqsched/\\

deadline\_algorithm\_Usched\)\.

Proof\.Admitted\.

EndSporadicEDFOptimality\.

The skeleton maps each extracted section to a correspondingProsaconstruct\. Definition 1 is encoded asvalid\_sporadic\_task, usingtask\_cost,task\_deadline, andtask\_min\_inter\_arrival\_timeforeie\_\{i\},did\_\{i\}, andpip\_\{i\}\. Definition 2 is encoded asrequest\_absolute\_deadline, representing the absolute deadlinet0\+dit\_\{0\}\+d\_\{i\}\. Definition 3 is encoded asfeasible, which quantifies over all legal arrival sequences\. Definition 4 is encoded asonline\_failure\_at, capturing missed deadlines, and Definition 5 is encoded asdeadline\_algorithm\_U, identified withProsa’sEDF\_schedule\. Lemma 1 is encoded asdeadline\_algorithm\_optimal, stating that feasibility is equivalent to success of the deadline algorithm on every legal request set\.

The surrounding type\-class context, includingTaskType,JobType, andTaskCost, connects these constructs toProsa’s scheduling framework\. TheAdmitted\.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 onProsa’sEDF\_optimalitytheorem\.

#### \-F4Proof Completion

In the final phase, we prompt the LLM to discharge theAdmittedobligations 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](https://arxiv.org/html/2608.12762#LST7):

Listing 7:Completed proof for the Optimality of the Deadline AlgorithmLemmadeadline\_algorithm\_optimal:

feasible<\-\>

\(forallarr\_seq:arrival\_sequenceJob,

valid\_arrival\_sequencearr\_seq\-\>

\(foralltsk,tsk\\ints\-\>respects\_sporadic\_task\_modelarr\_seqtsk\)\-\>

existssched:schedule\(ideal\.processor\_stateJob\),

valid\_scheduleschedarr\_seq/\\

all\_deadlines\_of\_arrivals\_metarr\_seqsched/\\

deadline\_algorithm\_Usched\)\.

Proof\.

rewrite/feasible/deadline\_algorithm\_U\.

split\.

\-move=\>FEASarr\_seqVALIDSPORADIC\.

apply:EDF\_optimality\.

have\[sched\[VALID\_SCHEDDEADLINES\_MET\]\]:=

FEASarr\_seqVALIDSPORADIC\.

byexistssched\.

\-move=\>EDF\_FEASarr\_seqVALIDSPORADIC\.

have\[sched\[VALID\_SCHED\[DEADLINES\_METEDF\_SCHED\]\]\]:=

EDF\_FEASarr\_seqVALIDSPORADIC\.

byexistssched\.

Qed\.

The proof follows the two directions of the equivalence\. First,rewrite /feasible /deadline\_algorithm\_Uunfolds the extracted definitions, reducing the statement to the relationship between general feasibility and existence of an EDF schedule\. In the forward direction, the assumptionFEASprovides some valid schedule that meets all deadlines for any legal arrival sequence\. The proof then appliesEDF\_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 satisfiesEDF\_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 lemmadeadline\_algorithm\_optimalis a validProsaformalization 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\-verifiedProsaproofs through a structured sequence of extraction, retrieval\-augmented skeleton generation, and targeted proof completion\.

### \-GDistribution of system invariants and their number of dependencies in the generated System Invariant Dataset

Figure[6](https://arxiv.org/html/2608.12762#A0.F6)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\.

![Refer to caption](https://arxiv.org/html/2608.12762v1/images/section_distribution.png)Fig\. 6:Distribution of system invariants and their dependencies\.
### \-HFine\-Grained Mapping from Raw Sketch Kinds toRocqKeywords

Table[VI](https://arxiv.org/html/2608.12762#A0.T6)presents the complete mapping from raw sketch kinds to their correspondingRocqkeywords, along with the rationale used in our normalization process\.

TABLE VI:Fine\-grained mapping from raw sketch kinds toRocqkeywords\.Raw Sketch KindRocqKeywordReasonDefinition familydefinitionDefinitionDirect equivalentformulaDefinitionA named mathematical formula = constant definitionequationDefinitionA named equation = defined constant/relationimplicit\_definitionDefinitionImplicitly defined conceptderived\_definitionDefinitionDerived from other definitionsfoundational\_equationDefinitionNamed base equation = constantrta\_equationDefinitionResponse\-time analysis equation = named bound constantcalculation\_formulaDefinitionA formula used in calculation = named constantderived\_formulaDefinitionDerived formula = defined constantresource\_planning\_formulaDefinitionFormula for planning = named constantobjective\_functionDefinitionOptimization objective = a function definitionoptimization\_objectiveDefinitionSame as objective\_functionderived\_functionDefinitionDerived non\-recursively \(not Fixpoint\)functionDefinitionNon\-recursive functionformulationDefinitionMathematical formulation = a definitiontask\_set\_definitionDefinitionExplicit definition of a task setinformal\_definitionDefinitionInformal but definitional in natureFixpoint familyalgorithmFixpointAlgorithms are recursive = Fixpointalgorithmic\_sketchFixpointSketch of a recursive algorithminformal\_algorithmic\_sketchFixpointInformal version of algorithmic\_sketchalgorithm\_sketchFixpointSame as algorithmic\_sketchalgorithm\_componentFixpointPart of a recursive algorithmalgorithm\_definitionFixpointDefines a recursive algorithmalgorithm\_descriptionFixpointDescribes an algorithmalgorithmic\_derivationFixpointAlgorithmically derived resultalgorithmic\_definitionFixpointFormally defined algorithmtransformation\_algorithmFixpointAn algorithm that transforms its inputmethodFixpointComputational method = procedureprocedureFixpointExplicit computational procedureheuristicFixpointIterative/recursive computational procedurerecurrenceFixpointRecurrence relation = recursive definitionLemma familylemmaLemmaDirect equivalentclaimLemmaA claim is an auxiliary provable factpropositionLemmaProposition = Lemma inRocqconventionobservationLemmaAn observation is an informal lemmapropertyLemmaA provable propositionstatementLemmaA mathematical statement to be provedformal\_statementLemmaFormal version of a statementconditionLemmaA provable condition/predicateconstraintLemmaProved inequality or boundcalculationLemmaResult of a calculation = proved equalityschedulability\_testLemmaDecidable test = proved as lemmaderived\_testLemmaA test derived from other resultsoptimization\_constraintLemmaProved inequality/boundoptimization\_claimLemmaClaim about an optimisationapplicationLemmaInstantiation of a resultinvariantLemmaSystem/loop invariants proved as lemmasremarkLemmaRemarks are informal lemmasfactLemmaA mathematical factresultLemmaA proved resultrestrictionLemmaA restriction = conditional lemmaconjectureLemmaUnproved; placeholder with Admittedproperty/constraintLemmaCombined property/constraintproblemLemmaDecision/optimisation problemruleLemmaInference rule = proved as lemmaoptimization\_problemLemmaProved bound/propertyschedulability\_conditionLemmaSchedulability condition = proved predicateproblem\_statementLemmaProblem stated formallyinequalityLemmaA proved inequalityknown\_resultLemmaExisting proved resultprincipleLemmae\.g\. scheduling principle = proved propertyderived\_rtaLemmaResponse\-time bounds are proved, not definedextensionLemmaExtends an existing lemmatransformationLemmaProved equivalence under transformationrefinementLemmaProved relationship between specificationsinformal\_sketchLemmaInformal sketch of a proof obligationinformalLemmaGeneric informal mathematical statementpolicyLemmaScheduling policy property = provable propositionincomplete\_malformed\_statementLemmaSafe fallbackTheorem / Corollary / Hypothesis familiestheoremTheoremDirect equivalentcorollaryCorollaryDirect equivalenthypothesisHypothesisDirect equivalentassumptionHypothesisExplicit assumption in aRocqSection contextTABLE VI:Fine\-grained mapping from raw sketch kinds toRocqkeywords \(continued\)\.