Technical Summary: PROVE-RT

Problem Statement

Safety-critical real-time systems (RTS) require rigorous schedulability analysis to ensure timing correctness. While mechanized verification using the PROSA/ROCQ framework offers a more reliable alternative to traditional pen-and-paper proofs, the manual construction of such proofs is prohibitively expensive. It requires substantial domain expertise and proof-engineering effort, with even minor model changes often invalidating existing proofs and necessitating extensive maintenance.

Although Large Language Models (LLMs) have shown promise in generating formal proofs for general mathematics and software verification, their application to real-time schedulability analysis faces three distinct challenges:

1. Data Scarcity: There is a lack of large-scale, mechanized training corpora specific to RTS, limiting LLMs' ability to learn PROSA-specific abstractions, terminology, and proof patterns.
2. Formalization Gap: Schedulability analyses in literature are expressed in non-mechanized forms (prose, equations, sketches) that lack the explicit structural requirements (variables, hypotheses, type-class instances, dependency ordering) mandated by the ROCQ theorem prover.
3. Structural Complexity: Schedulability lemmas involve deep hierarchies of task models, workload definitions, and interference bounds. Generating a valid proof requires not just tactic selection but the construction of a correct dependency-ordered context, which is significantly more complex than standard theorem proving.

Methodology: The PROVE-RT Framework

PROVE-RT is an LLM-assisted framework designed to automate the generation of dependency-ordered PROSA/ROCQ scripts from informal schedulability analyses. The framework operates through a five-stage pipeline:

1. System Invariant Extraction:
   The input schedulability analysis is processed by an LLM to extract a set of system invariants (definitions, lemmas, theorems) and their corresponding informal sketches. These sketches describe the statement, intuition, and proof outline of each invariant. Crucially, the system constructs a Dependency Graph (DAG) to determine the strict ordering in which invariants must be formalized, ensuring that prerequisites are introduced before dependent constructs.

2. PROSA Documentation Processing:
   To address the lack of domain-specific context, the PROSA library documentation is processed into a retrieval-ready corpus. This involves structure-aware chunking:

   • Proof-Oriented Chunking: For modules like Analysis and Results, code blocks are paired with descriptive text to preserve the link between proofs and their motivations.
   • Section-Level Chunking: For other modules, smaller, self-contained sections are used.
   • Dependency Recovery: For proof-oriented modules, the system performs syntax-aware recovery to identify and include necessary preceding definitions and type-class contexts required for a retrieved fragment to be valid.

3. Retrieval-Augmented Generation (RAG):
   For each invariant, the framework constructs a retrieval query based on the informal sketch (statement, intuition, conclusion). It retrieves relevant documentation fragments and proof examples from the processed corpus to provide the LLM with library-specific definitions, assumptions, and proof patterns.

4. Staged Skeleton Generation:
   The framework decouples structure generation from proof generation. The LLM first generates a structurally valid skeleton for each invariant.

   • Rules: All proof-bearing constructs (lemmas/theorems) are generated with deferred obligations (Admitted.), while non-proof constructs (definitions) are fully specified.
   • Integrity: The system enforces rules to prevent the model from turning claims into unsupported assumptions.
   • Validation: Skeletons are compiled with coqc to verify type correctness and structural validity before proceeding.

5. Proof Completion with Iterative Repair:
   Once a valid skeleton is established, the LLM is prompted to discharge the deferred Admitted. obligations. This stage utilizes iterative repair: if the generated proof fails to compile, the compiler error messages are fed back to the LLM to guide corrections. A proof-integrity checker ensures the model does not circumvent the proof obligation by introducing unsupported axioms or shifting the burden to new global definitions.

Key Contributions

1. PROVE-RT Framework: The first LLM-assisted framework specifically targeting the mechanization of RTS schedulability analyses in PROSA/ROCQ. It introduces a staged approach (sketching, skeleton generation, proof completion) combined with dependency-aware retrieval.
2. System Invariant Dataset: The construction of a large-scale corpus derived from 1,191 real-time systems papers, containing 13,134 informal sketches with explicit dependency information. This dataset addresses the critical lack of domain-specific data for training and evaluating mechanization tools.
3. Empirical Analysis of Challenges: A detailed study of failure modes in LLM-based mechanization, highlighting the insufficiency of direct prompting and the necessity of retrieval guidance and dependency ordering.

Experimental Results

The framework was evaluated on a curated subset of 300 informal sketches representing various schedulability analysis categories (e.g., response-time analysis, EDF, FIFO).

• Baseline Performance: Direct prompting of state-of-the-art LLMs (GPT-5, Claude-Opus-4.6) failed to reliably generate valid PROSA scripts. GPT-5 achieved a 0.0% success rate, and Claude-Opus-4.6 achieved only 0.33%. Notably, many "successful" compilations from baselines did not utilize the PROSA library, merely generating generic ROCQ code.
• PROVE-RT Performance: Using dense retrieval (semantic embeddings), PROVE-RT achieved a 44.7% success rate (134/300 sketches fully mechanized).
  • BM25 retrieval achieved 42.0%.
  • Hybrid retrieval achieved 41.0%.
• Impact of Complexity: Success rates decreased as the number of sections (dependency depth) in a sketch increased, indicating that longer dependency chains remain a significant challenge. However, PROVE-RT successfully mechanized several multi-section sketches, demonstrating its ability to handle non-trivial dependency structures.
• Retrieval Efficacy: Dense retrieval was most effective for end-to-end success, particularly for definitions, while sparse (BM25) and hybrid methods showed strength in retrieving exact lemma names and identifiers for proof-bearing constructs.

Significance and Claims

The paper claims that PROVE-RT demonstrates that retrieval-guided and staged LLM assistance can significantly improve the automated mechanization of schedulability analysis compared to direct prompting. By decomposing the task into dependency-aware sketching, skeleton generation, and iterative proof repair, the framework overcomes the formalization gap between informal literature and rigorous theorem proving.

The authors position PROVE-RT not as a complete solution that eliminates human effort, but as a significant step toward reducing the barrier to entry for mechanized verification in real-time systems. The constructed dataset is highlighted as a critical resource to facilitate future research in LLM-assisted formalization for this domain. The work also suggests potential for using such frameworks to verify AI-generated schedulability analyses, adding a layer of trust to generative AI in safety-critical domains.