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

This paper introduces PROVE-RT, an LLM-assisted framework for generating mechanized theorem prover scripts for real-time systems schedulability analysis using the PROSA/ROCQ proof assistant. The paper addresses the challenge that schedulability analysis, while essential for certifying real-time systems, is typically developed through pen-and-paper proofs that are difficult to scale, validate, and maintain. Mechanized verification in PROSA/ROCQ offers a rigorous alternative, but manually constructing such proofs requires substantial domain expertise and proof-engineering effort.

The paper identifies three key challenges in this domain: (i) limited mechanized RTS corpora, restricting LLM understanding of PROSA abstractions and proof patterns; (ii) a formalization gap between structurally non-mechanized schedulability analyses and PROSA's explicit proof structure; and (iii) the complexity in the structure of schedulability lemmas/theorems compared to mathematical theorem-proving tasks.

To overcome these challenges, PROVE-RT incrementally mechanizes schedulability analyses through staged formalization, dependency-aware proof construction, and retrieval-augmented grounding using RTS knowledge and PROSA documentation. The framework consists of five stages: (1) extracting system invariants, informal sketches, and dependency graphs from formally written schedulability analyses; (2) processing the PROSA documentation into retrieval-ready fragments; (3) retrieving relevant documentation and examples with dependency recovery for proof-oriented modules; (4) generating and validating a structurally correct proof skeleton with deferred obligations; and (5) completing the deferred proofs using iterative repair.

The paper makes three main contributions. First, it introduces PROVE-RT, which is described as the first LLM-assisted framework targeting the PROSA-based mechanization of RTS analysis. Second, it develops a benchmark from 1,191 real-time systems papers, comprising 13,134 mechanization-oriented informal sketches and corresponding PROSA/ROCQ script artifacts. Third, it analyzes key challenges, recurring failure modes, and corner cases encountered when generating PROSA/ROCQ scripts with LLMs.

For the system invariant dataset construction, the paper collected schedulability-analysis papers from established real-time systems venues including RTSS, RTAS, ECRTS, EMSOFT, RTCSA, RTNS, RSS, and IROS using the IEEE Xplore API. After filtering, the retained corpus contained 1,191 papers and 13,134 informal sketches. The extraction process produced invariants across six normalized categories: definitions (51.9%), lemmas (31.6%), theorems (13.9%), corollaries (1.7%), fixpoints (0.9%), and hypotheses (0.1%).

The evaluation used a curated subset of 300 unit-level informal sketches selected via proportional stratified sampling over dependency-depth categories from a larger curated corpus of 109 papers and 1,904 sketches. The evaluation compared PROVE-RT against direct LLM-based generation using GPT-5 and Claude-Opus-4.6. The results show that direct prompting of state-of-the-art LLMs fails to reliably generate valid PROSA mechanizations. Specifically, GPT-5 formalized 0 out of 300 sketches (0.0%) whether prompted with paper statements or informal sketches, while Claude-Opus-4.6 formalized only 1 out of 300 sketches (0.33%).

In contrast, PROVE-RT achieved substantially better results. With dense retrieval, it mechanized 134 out of 300 sketches, achieving a success rate of 44.7%. With BM25 retrieval, it mechanized 126 sketches (42.0%), and with hybrid retrieval, it mechanized 123 sketches (41.0%). The paper notes that given that PROVE-RT operates in the specialized and low-resource setting of PROSA-based real-time systems mechanization, a 44.7% success rate indicates substantial progress.

An interesting observation from the evaluation was that both GPT and Claude often produced compilable ROCQ scripts without actually using PROSA. Claude produced compilable scripts for 39 of the 300 informal sketches, but only 1 used PROSA; the remaining 38 were generic compilable ROCQ scripts. GPT generated 148 compilable ROCQ scripts out of 300 attempts, but none used PROSA. The paper counts such outputs as failures since the goal is to mechanize analyses within PROSA.

Regarding dependency depth (RQ2), the paper found that success decreases as sketches contain more sections, suggesting that deeper dependency chains make mechanization harder. However, PROVE-RT still succeeded on several multi-section sketches, indicating that its dependency-aware extraction, retrieval, and staged generation strategy can support nontrivial schedulability-analysis mechanization.

Regarding retrieval methods (RQ3), the paper found that dense retrieval achieves the best end-to-end mechanization performance (44.7%), while hybrid retrieval compiles the most individual sections (608 out of 1393, or 43.6%). The paper notes that dense retrieval is most effective for semantic alignment, whereas sparse and hybrid retrieval remain valuable for proof-bearing constructs that depend on exact PROSA references. For proof-bearing constructs specifically, BM25 proved 12 out of 22 sketches (54.5%), hybrid proved 11 out of 22 (50.0%), and dense proved 9 out of 22 (40.9%).

The paper concludes that direct prompting of state-of-the-art LLMs is insufficient for reliable PROSA generation, while PROVE-RT achieves a success rate of 44.7% with dense retrieval. It also constructs a mechanization-oriented corpus of informal sketches with dependency information that "can facilitate future research on LLM-assisted mechanization of schedulability analyses, as domain-specific datasets for PROSA/ROCQ-based schedulability analysis are currently lacking and remain a major bottleneck for automated script generation."

Future work will improve retrieval, incorporate richer proof-state feedback, extend the framework to broader classes of schedulability analyses, and study the capabilities of LLMs to generate schedulability constraints for new scheduling problems, for which PROVE-RT can be used to mechanically verify the correctness of LLM-generated schedulability results.

Improvements to AI systems:

1. Staged formalization with dependency-aware generation: Implement a multi-stage pipeline that first extracts invariants, informal sketches, and dependency graphs from natural-language analyses, then constructs proof skeletons with deferred obligations before filling in proofs. This allows the AI to handle complex, multi-step formal proofs by breaking them into manageable, sequentially dependent sub-tasks, reducing error propagation.

2. Retrieval-augmented grounding with domain-specific corpora: Integrate dense and sparse retrieval over a curated corpus of mechanization-oriented sketches, documentation fragments, and proof patterns. The AI can dynamically retrieve relevant PROSA/ROCQ definitions, lemmas, and proof idioms during generation, improving semantic alignment and reducing hallucination of non-existent or incorrect proof constructs.

3. Proof-structure validation with deferred obligations: Add a validation layer that checks structural correctness of generated proofs (e.g., correct theorem statements, dependency ordering) before attempting full proof completion. The AI can defer unsolved sub-goals, then iteratively repair them using proof-state feedback, enabling incremental progress on hard proofs instead of all-or-nothing generation.

4. Failure-mode-aware generation with fallback strategies: Train or prompt the AI to recognize recurring failure modes (e.g., generating compilable but PROSA-agnostic scripts, missing dependency chains, incorrect fixpoint handling). The system can then switch retrieval strategies (e.g., from dense to BM25 for proof-bearing constructs) or re-prompt with additional context, improving robustness in low-resource formal domains.

5. Benchmark-driven fine-tuning and evaluation: Use the constructed corpus of 13,134 informal sketches and 1,904 curated sketches with dependency-depth labels to fine-tune LLMs specifically for PROSA/ROCQ mechanization. The AI can be evaluated against stratified benchmarks (e.g., by dependency depth) to identify and improve performance on harder, multi-section proofs.

What the improved AI system can do:

• Automatically generate mechanized, machine-checkable proofs for real-time systems schedulability analyses in PROSA/ROCQ, achieving a success rate of 45% on complex, unseen sketches (vs. 0–0.33% for direct prompting).

• Handle multi-section analyses with deep dependency chains by decomposing them into staged formalization, retrieving relevant PROSA documentation on demand, and iteratively repairing deferred proof obligations.

• Distinguish between generic compilable scripts and true PROSA-based mechanizations, avoiding false positives by validating that generated proofs actually use PROSA abstractions and invariants.

• Adapt its retrieval strategy based on the proof construct type (e.g., dense for semantic alignment, BM25 for exact PROSA references), improving success on proof-bearing lemmas and theorems.

• Provide a reusable, dependency-aware dataset and benchmark for future LLM research on formal verification of real-time systems, enabling reproducible evaluation and targeted fine-tuning.

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