Pith. sign in

REVIEW 4 major objections 7 minor 109 references

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

T0 review · 4 major / 7 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read PROVE-RT is an LLM-assisted framework that claims to be the first to automatically generate machine-checked PROSA/Rocq proof scripts for real-time schedulability analyses, succeeding on 44.7% of a 300-case curated evaluation where direct…

desk verdict PROVE-RT is a genuinely new target and a reusable corpus, but the 44.7% headline is mostly definitions and the sketches are unvalidated, so the central mechanization claim is not yet established; send to review, expect revision. read the letter →

arxiv 2608.12762 v1 pith:SJHCXE6G submitted 2026-08-13 cs.AI

Sadat Shahriyar , Shareef Ahmed , Abdullah Al Arafat This is my paper · ORCID
classification cs.AI
keywords mechanizedverificationschedulabilityanalysisreal-timesystemsLLM-assistedtheoremprovingPROSARocq/Coqscriptsretrieval-augmentedgenerationinformalsketches
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

PROVE-RT sets out to do what has not been done before: take schedulability analyses from real-time systems papers and turn them, automatically, into proof scripts that the PROSA/Rocq mechanized-verification library accepts. The paper's central claim is that this is achievable with LLM assistance if generation is guided by dependency-aware informal sketches, retrieval from PROSA documentation, and a two-stage skeleton-then-proof pipeline. On a curated evaluation of 300 informal sketches, the framework mechanizes 134 (44.7%), while direct prompting of frontier LLMs produces essentially no valid PROSA scripts. If the claim holds, it means the expensive, error-prone step of hand-writing mechanized schedulability proofs can be substantially automated, and the same pipeline can later serve as a verification layer for AI-generated scheduling results.

What carries the argument

The load-bearing object is the dependency-aware informal sketch. For each extracted invariant—definition, lemma, theorem, corollary, fixpoint, or hypothesis—the sketch records the statement, the intuition, the proof outline, and the identifiers it depends on, and these dependencies form a directed acyclic graph that fixes the order in which code blocks must appear. Because Rocq is forward-referencing, the DAG ordering is what makes the generated script compilable at all. Around that object, the pipeline has three further mechanisms: retrieval over a processed PROSA documentation corpus (chunked proof-oriented vs section-level, with syntax-based dependency recovery), skeleton generation that forces every proof obligation to remain an "Admitted" placeholder while definitions and type-class contexts are fully elaborated, and a proof-completion stage that fills the placeholders in batch and repairs failures from compiler error messages under a proof-integrity checker.

What would settle it

Take a random sample of the 300 evaluated sketches, compare each sketch's assumptions against the source paper's stated hypotheses, and recompile the generated scripts with any omitted hypotheses reinstated; if a substantial fraction of scripts then fail, the success rate measures fidelity to the sketch rather than mechanization of the original analyses.

Watch

Extended reading notes

Core claim

The paper claims that the reason LLMs fail at PROSA/ROCQ script generation is not lack of proof ability but lack of the recovered formal structure: schedulability analyses in the literature are written for human readers, with assumptions, definitions, and dependencies left implicit. PROVE-RT's contribution is an intermediate representation that makes that structure explicit—each extracted invariant is paired with an informal sketch and a dependency edge, ordered into a DAG, and then fed into retrieval-augmented skeleton generation in which proof bodies are deferred with "Admitted", followed by batch proof completion with compiler-guided repair. Against direct prompting (0/300 for one tested frontier model, 1/300 for another), PROVE-RT with dense retrieval succeeds on 134/300 sampled sketches (44.7%). The paper takes this as evidence that retrieval-guided, staged LLM assistance is the right route to automated mechanization of real-time schedulability analysis in PROSA/Rocq.

Load-bearing premise

The measured success rate stands or falls with the informal sketches: they are produced by an LLM and filtered only by a deterministic structural check, with no human validation, so if a sketch silently weakens or omits an assumption from the original paper, a script that compiles proves the sketch, not the published analysis.

Editorial extensions

If this is right

  • Direct prompting is not a viable route: on the 300-sketch evaluation, the tested frontier models produced no usable PROSA mechanizations (0/300 and 1/300), while PROVE-RT's best variant succeeded on 134/300.
  • Dependency depth is the main difficulty: success rates drop as sketches contain more sections, yet multi-section chains are still mechanized, so the framework handles nontrivial dependency structures, not just isolated definitions.
  • Retrieval method matters in a task-specific way: dense retrieval wins end-to-end (44.7%), while sparse and hybrid retrieval are stronger on proof-bearing lemmas and theorems that need exact PROSA identifiers.
  • The corpus of 1,191 papers and 13,134 dependency-annotated informal sketches becomes a reusable benchmark for future work on LLM-assisted formalization in real-time systems.
  • If the claim holds, PROVE-RT offers a path to reduce the proof-engineering burden documented in prior PROSA-based efforts, such as the thousands of lines of Rocq code needed to connect analyses to certified operating-system kernels.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Because the evaluation set was curated to categories well aligned with existing PROSA abstractions, the 44.7% figure is best read as an upper bound for current capability; an uncurated corpus would likely score lower.
  • The same staged skeleton-and-repair pattern should transfer to other domain-specific proof libraries that enforce forward referencing, so the method is not inherently tied to PROSA.
  • The framework's most consequential use may be the one the paper mentions in passing: serving as a mechanical check on schedulability claims produced by generative AI, turning the LLM from author of an analysis into author of a candidate that a trusted kernel verifies.
  • A natural stress test is to apply the pipeline to the integration-style proofs that dominate PROSA's real-world cost, such as translation interfaces to verified kernels, where the recovered formal structure is the hard part.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 7 minor

Summary. This paper presents PROVE-RT, an LLM-assisted pipeline that generates PROSA/Rocq mechanizations of schedulability analyses from real-time systems papers. The pipeline comprises five stages: LLM-based extraction of system invariants, informal sketches, and dependency graphs; processing of PROSA documentation into retrieval-ready chunks; retrieval-augmented context construction with a syntax-aware dependency-recovery step; staged skeleton generation in which proof obligations are deferred with Admitted; and batched proof completion with compiler-guided repair plus a proof-integrity checker. The authors contribute a corpus of 13,134 informal sketches extracted from 1,191 papers and evaluate the framework on 300 curated sketches, reporting a 44.7% end-to-end success rate with dense retrieval versus 0% and 0.33% for direct-prompting baselines using GPT-5 and Claude-Opus-4.6. They also report a dependency-depth analysis (RQ2) and a comparison of BM25, dense, and hybrid retrieval (RQ3), with per-construct results in Table IV and a limitations discussion in Section IX.

Significance. The contribution is timely: to my knowledge this is the first LLM-assisted framework aimed at PROSA/Rocq mechanization of schedulability analyses, and the corpus and evaluation support future work. The paper's strengths are substantial: correctness of generated scripts is grounded by the Rocq compiler rather than by the LLM; the direct-prompting baselines are genuine and fairly described; per-construct results are reported transparently in Table IV; and Section IX states clear limitations. If the central claim were fully supported, the framework would reduce the documented proof-engineering burden of PROSA-based verification. However, the headline success rate is dominated by definition formalization (278 of 300 evaluation sketches), and the fidelity of the LLM-extracted sketches to the source papers is not validated, so the evidence supports a narrower claim than the abstract makes. These issues are addressable within the manuscript's scope, which is why I recommend major revision rather than rejection.

major comments (4)
  1. [Table IV; Section VIII-A] Table IV shows that 278 of the 300 evaluation sketches (92.7%) are definitions, and the headline success rate of 44.7% (Dense) is dominated by them: for a definition there is no proof obligation, so a 'success' requires only that the generated skeleton and definition body type-check, and the proof-completion stage contributes nothing. For the 22 proof-bearing sketches, the Dense configuration succeeds on only 9 (40.9%), including just 1 of 3 theorems, while BM25 succeeds on 12 of 22 (54.5%). The abstract's claim that PROVE-RT 'achieves a success rate of 44.7%' at mechanizing schedulability analyses therefore overstates the demonstrated capability. The paper should report the success rate separately for definition-only and proof-bearing sketches and should lead the quantitative claims with the proof-bearing rates.
  2. [Section VII-A; Section VIII] The evaluation assumes that the 300 informal sketches are faithful, nontrivial representations of the schedulability analyses in the source papers, and this assumption is load-bearing but not established. The sketches were produced by Gemini-2.5-Flash and passed only a deterministic structural filter based on dependency resolution (exact, normalized, and fuzzy matching with a 0.88 threshold, and an unresolved-dependency rejection ratio of 0.15); no human validation against the source papers is reported, and the human-in-the-loop curation described in Section VIII is a category-level selection step rather than a sketch-fidelity check. Because both the skeleton statement and the completed proof are generated from the sketch, a compiling script establishes only that the sketch is internally consistent: neither the Rocq compiler nor the proof-integrity checker can detect a weakened statement or a missing assumption, since neither has access to the original paper. I recommend adding a human-validated fidelity sample with agreement rates, or explicitly reframing the contribution as the mechanization of LLM-extracted sketches rather than of the papers' analyses.
  3. [Section VIII; Table II] The comparison between PROVE-RT and the direct-prompting baselines is input-asymmetric in a way that can inflate the reported gap. The baselines are given the original paper text or the raw informal sketch, whereas the end-to-end PROVE-RT run also includes the extraction stage; if extraction simplifies the analysis, part of the difference between 0% and 44.7% may reflect input simplification rather than the value of the retrieval, skeleton, and repair components. The near-absence of Hypothesis constructs in the corpus (8 of 13,134 in Table I) is one indication that the extractor may systematically omit assumptions. To separate these effects, the paper should quantify the simplification introduced by the extraction stage, for example by running the PROVE-RT pipeline on the original paper text as input or by measuring the complexity reduction between the papers and their extracted sketches.
  4. [Section IX; Section VI] The paper's own evidence and examples delimit the central claim more sharply than the abstract. Section IX concedes that 'deeper dependency chains and proof-bearing constructs that require precise PROSA context' remain difficult, and Table IV shows that the best overall configuration proves only 1 of 3 theorem sketches. The worked example in Section VI is a definitional identity discharged by unfold followed by lia, and the Appendix F example discharges its theorem by applying PROSA's pre-existing EDF_optimality result; neither demonstrates that the framework mechanizes a substantive schedulability analysis whose proof must be synthesized. The conclusions should be calibrated to the proof-bearing results and should state what fraction of the proof-bearing successes consist of direct application of existing PROSA theorems rather than multi-step proof synthesis.
minor comments (7)
  1. [References] References [14] and [44] are the same paper, as are [16] and [45]; the duplicate entries should be removed and the citations consolidated.
  2. [Reference [6]] Reference [6] cites the ROCQ 9.2.0 reference manual, while Section VII-D reports the evaluation used ROCQ version 9.1.0; please reconcile this inconsistency.
  3. [Figure 5] Figure 5 restricts the plot to sketches with at most 10 sections, which excludes 30 of the 300 evaluation sketches; the caption should state this count explicitly and the text should confirm that the decreasing trend holds for the excluded group.
  4. [Section VII-D] The evaluation depends on closed commercial models (Gemini-2.5-Flash, Claude-Opus-4.6, GPT-5) but the exact prompts, model temperatures, and decoding settings are not given; including these, together with the full prompt templates, in an appendix would materially improve reproducibility.
  5. [Section V-C] The fuzzy-matching threshold (0.88), the unresolved-dependency rejection ratio (0.15), the retrieval top-K (K=5), and the weight ordering alpha > beta > gamma are introduced without sensitivity analysis; a short ablation study would clarify how sensitive the reported rates are to these choices.
  6. [Section VI; Appendix A] The assumptions listed in the extracted sketch for the motivating example (for example, 'faults are detected immediately upon occurrence') do not appear anywhere in the generated skeleton or proof; please clarify how sketch assumptions are intended to be mapped into the formal development.
  7. [Listing 6] Listing 6 contains 'tsk \ints -> respects_sporadic_task_model arr_seq tsk', which appears to be a rendering artifact for 'tsk \in ts'; please check all listing renderings in the final version.

Circularity Check

2 steps flagged · score 4.0 of 10

Evaluation targets and the worked example are defined from LLM-generated restatements: compiling scripts for extracted informal sketches is presented as mechanizing the literature, and the illustrative proof is a definitional equality.

  1. self definitional [Section IV-B (success criterion), VII-A (dataset construction), VIII-A (evaluation subset)]
    "A successful output must satisfy three requirements. First, each generated code block s_j must correctly represent the corresponding extracted invariant i_j. In our implementation, we used Gemini-2.5-Flash as the LLM and prompted it to identify candidate system invariants I from each schedulability analysis and to extract their summaries, informal sketches K_j, and dependency information for constructing G_D. PROVE-RT achieves the best performance among the evaluated approaches when used with dense RAG, mechanizing 134 informal sketches and achieving a success rate of 44.7%."

    Section IV-B defines a successful output as correctly representing the extracted invariant i_j, and Section VII-A shows i_j, K_j, and G_D are produced by Gemini-2.5-Flash and filtered only by a structural dependency validator. The evaluation set in Section VIII-A is sampled from those sketches. Therefore the 'schedulability analysis' being mechanized is the LLM's own informal restatement; the original paper's text enters only through that unvalidated extraction. The Rocq compiler and proof-integrity checker verify consistency between script and sketch, not between script and source paper; they cannot detect a weakened statement or a theorem turned into a definition.

  2. self definitional [Section VI-C and VI-D, Listings 1-2]
    "Definition 1 is realized as the function W_i_k_i, which takes the fault-tolerance overhead A_i_k_i as an argument and returns its sum with the failure-free WCET W_i_0. Claim 1 is stated as Lemma W_i_k_i_retry, which asserts that instantiating W_i_k_i with the retry-specific overhead yields exactly Equation (2). The proof proceeds in two steps. First, unfold W_i_k_i δ-reduces the definition, exposing the underlying goal ... This is an equality over natural numbers that follows directly from the commutativity of addition."

    In Listing 1, W_i_k_i is defined as W_i_0 + A_i_k_i, and the lemma W_i_k_i_retry states W_i_k_i (k_i * (R_star + W_i_0)) = k_i * (R_star + W_i_0) + W_i_0. The paper's own proof is 'unfold W_i_k_i. lia.', i.e., the claim is a definitional expansion plus commutativity. No formal model of tasks, faults, restarts, or overhead A_i_k_i is introduced, so Equation (2) from [43] is not derived from retry semantics; it is made true by the way the definition was chosen. The worked example therefore demonstrates a tautology, and it illustrates how definition-heavy extracted sketches can produce scripts that compile without mechanizing the underlying schedulability argument.

full rationale

The paper has two genuinely independent components: the Rocq compiler is an external checker, and the comparison against direct prompting is a real baseline. There is no self-citation chain and no fitted parameter renamed as a prediction. However, the central claim 'mechanize schedulability analyses in real-time systems literature' is anchored to informal sketches produced by Gemini-2.5-Flash with only a deterministic structural filter (Section VII-A); the 300-unit evaluation set is sampled from those sketches, and Section IV-B defines success as representing the extracted invariant. A compiling script therefore certifies internal consistency with the LLM's restatement, and the proof-integrity checker has no access to the original paper to detect weakened or definitionally-true reformulations. This is reinforced by the worked example (Section VI), where Claim 1 is true by unfolding the definition of W_i_k_i plus commutativity, not by formalizing retry semantics. Table IV shows 278/300 evaluation sketches are definitions, for which proof completion is vacuous, and Section IX concedes limited success on proof-bearing constructs. Thus the headline number is partially self-referential, although not a derivation equivalent to its input; the direct-prompting baselines and compiler acceptance give the empirical comparison some independent content. Score 4.

Assumptions & free parameters 6 free parameters · 4 assumptions · 0 invented entities

The central claim rests on procedural assumptions rather than physical entities. The most important is that LLM-generated informal sketches are faithful enough to serve as ground truth for mechanization. The listed free parameters are all engineering choices that affect the reported success rate, but none is fitted to the final evaluation numbers.

free parameters (6)
  • Retrieval top-k K = 5
    Number of documentation chunks retrieved per query (Section VII-D). No sensitivity analysis is reported, and success rates may depend on this choice.
  • Dependency weighting coefficients alpha, beta, gamma = not reported, alpha > beta > gamma
    Weights for type-level, explicit-reference, and proof-token zones in dependency recovery (Section V-C). The values are hand-chosen and not swept.
  • Fuzzy dependency matching threshold = 0.88
    Threshold for linking normalized dependency strings to identifiers during corpus validation (Section VII-A).
  • Unresolved-dependency rejection ratio = 0.15
    Papers with an unresolved-dependency ratio above 0.15 are rejected from the corpus (Section VII-A).
  • Retry budgets M_s and M_b = not specified
    Number of regeneration and repair attempts for skeleton generation and proof completion (Algorithms 1 and 2). Budget exhaustion marks sections as failed.
  • Stratified sampling seed = 42
    Fixed seed used to sample 300 sketches from 1,904 curated sketches (Section VIII-A). No other seeds are tested, so the headline number has no variance estimate.
assumptions (4)
  • ad hoc to paper Gemini-2.5-Flash extracted informal sketches and dependency graphs faithfully represent the source papers' schedulability analyses.
    The benchmark and evaluation are built on LLM extraction with only a deterministic structural filter and no reported human verification of sketch fidelity (Section VII-A).
  • domain assumption The 300 sampled sketches are representative of mechanization difficulty across schedulability analyses.
    Sampling is stratified by dependency depth over a human-curated subset aligned with PROSA abstractions (Section VIII-A), so it may not generalize to all schedulability analyses.
  • domain assumption Rocq compilation plus the proof-integrity checker is a sufficient criterion for successful mechanization.
    Compilation proves internal consistency of the generated script, but not that the generated statement matches the source paper (Sections V-E and VIII-C).
  • domain assumption The processed PROSA documentation corpus contains the definitions and lemmas needed for the target analyses.
    Retrieval can only succeed if relevant PROSA constructs are present in the 5,097 fragments from 356 PROSA source files (Section VII-D).

how reviews work

0 comments
Cite this review

Pith. "Pith review of PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs." pith.science (2026). https://pith.science/paper/SJHCXE6G

@misc{pith2026260812762,
  author       = {Pith},
  title        = {Pith review of: PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SJHCXE6G}},
  note         = {Machine review of arXiv:2608.12762}
}
read the original abstract

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

Figures

Figures reproduced from arXiv: 2608.12762 by the authors.

Figure 1
Figure 1. Overview of the proposed PROSA/ROCQ proof￾generation pipeline. V. PROVE-RT FRAMEWORK PROVE-RT consists of five stages: (1) Extracting system invariants, informal sketches, and dependency graph from formally written schedulability analysis; (2) Processing the PROSA documentation into retrieval-ready fragments; (3) re￾trieving relevant documentation and examples, with depen￾dency recovery for proof-oriented modules; (… view at source ↗
Figure 2
Figure 2. Skeleton code generation fails, the section is regenerated; sections that repeatedly fail are logged and skipped so that the pipeline can continue. E. Skeleton Code Completion After skeleton generation, each code block sj may contain proof-bearing constructs whose proof bodies are deferred using Admitted. The goal of the completion stage is to generate a proof fragment πj that replaces each deferred proof and makes … view at source ↗
Figure 3
Figure 3. Batch Completion with Iterative Repair If compilation fails or any violation is reported by the proof￾integrity checker, PROVE-RT enters an iterative repair loop in which compiler feedback guides corrections. At each iteration, the error message and its location are extracted from the compiler output and incorporated into a repair prompt together with the informal sketch Kj and the retrieved context Rj . The LLM the… view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: System Invariant Dataset Collection potheses, lemmas, theorems, corollaries, and fixpoints. The complete fine-grained mapping from raw sketch kinds to ROCQ keywords is provided in Appendix H. Overall, the extraction process produced 13,134 normalized system invari￾ants…
Figure 5
Figure 5. Figure 5: Mechanization success by dependency depth for different retrieval methods. For readability, the plot shows sketches [PITH_FULL_IMAGE:figures/full_fig_p013_5.png]
Figure 6
Figure 6. Figure 6: Distribution of system invariants and their dependencies. [PITH_FULL_IMAGE:figures/full_fig_p027_6.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

109 extracted references · 60 canonical work pages

  1. [1]

    Liu and layland’s schedulability test revisited,

    R. Devillers and J. Goossens, “Liu and layland’s schedulability test revisited,”Inf. Process. Lett., vol. 73, no. 5–6, p. 157–161, Mar. 2000. [Online]. Available: https://doi.org/10. 1016/S0020-0190(00)00016-8

  2. [2]

    Message response time analysis for ideal controller area network (can) refuted,

    R. J. Bril, J. J. Lukkien, R. I. Davis, and A. Burns, “Message response time analysis for ideal controller area network (can) refuted,” 2006. [Online]. Available: https: //api.semanticscholar.org/CorpusID:9850815

    2006

  3. [3]

    Timing analysis of fixed priority self-suspending sporadic tasks,

    G. Nelissen, J. Fonseca, G. Raravi, and V . N ´elis, “Timing analysis of fixed priority self-suspending sporadic tasks,” in 2015 27th Euromicro Conference on Real-Time Systems, 2015, pp. 80–89

    2015

  4. [4]

    Many suspensions, many problems: a review of self- suspending tasks in real-time systems,

    J.-J. Chen, G. Nelissen, W.-H. Huang, M. Yang, B. Brandenburg, K. Bletsas, C. Liu, P. Richard, F. Ridouard, N. Audsley, R. Rajkumar, D. Niz, and G. Br ¨uggen, “Many suspensions, many problems: a review of self- suspending tasks in real-time systems,”Real-Time Syst., vol. 55, no. 1, p. 144–207, Jan. 2019. [Online]. Available: https://doi.org/10.1007/s11241...

    work page doi:10.1007/s11241-018-9316-9 2019

  5. [5]

    Prosa: A case for readable mechanized schedulability analysis,

    F. Cerqueira, F. Stutz, and B. B. Brandenburg, “Prosa: A case for readable mechanized schedulability analysis,” in2016 28th Euromicro Conference on Real-Time Systems (ECRTS), 2016, pp. 273–284. [6]The Rocq Prover, 2026, available at https://rocq-prover.org/doc/ V9.2.0/refman/index.html. Last accessed: 2026-05-21

    2016

  6. [6]

    Intuition for generating code: Each sporadic task can release jobs at arbitrary times, but not too frequently

    e_i <= p_i Conclusion: Defines the sporadic task model and the task-system model. Intuition for generating code: Each sporadic task can release jobs at arbitrary times, but not too frequently. The parameter p_i prevents infinitely dense releases, while e_i and d_i describe how much processor time each released job needs and when it must complete. Steps fo...

    work page

  7. [7]

    Certican certifying can analyses and their results,

    P. Fradet, X. Guo, and S. Quinton, “Certican certifying can analyses and their results,”Real-Time Syst., vol. 59, no. 2, p. 160–198, Mar. 2023. [Online]. Available: https: //doi.org/10.1007/s11241-023-09393-2

    work page doi:10.1007/s11241-023-09393-2 2023

  8. [8]

    Integrating formal schedulability analysis into a verified os kernel,

    X. Guo, M. Lesourd, M. Liu, L. Rieg, and Z. Shao, “Integrating formal schedulability analysis into a verified os kernel,” in Computer Aided Verification, I. Dillig and S. Tasiran, Eds. Cham: Springer International Publishing, 2019, pp. 496–514

    2019

Show all 109 references
  1. [9]

    Abstract response-time analysis: A formal foundation for the busy-window principle (artifact),

    S. Bozhko and B. B. Brandenburg, “Abstract response-time analysis: A formal foundation for the busy-window principle (artifact),”Dagstuhl Artifacts Ser., vol. 6, pp. 03:1–03:2, 2020. [Online]. Available: https://api.semanticscholar.org/CorpusID: 220275236

    2020

  2. [10]

    Nipkow, M

    T. Nipkow, M. Wenzel, and L. C. Paulson,Isabelle/HOL: a proof assistant for higher-order logic. Berlin, Heidelberg: Springer-Verlag, 2002

    2002

  3. [11]

    The lean theorem prover (system description),

    L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer, “The lean theorem prover (system description),” inAu- tomated Deduction - CADE-25, A. P. Felty and A. Middeldorp, Eds. Cham: Springer International Publishing, 2015, pp. 378– 388

    2015

  4. [12]

    Towards a practical programming language based on dependent type theory,

    “Towards a practical programming language based on dependent type theory,” 2007. [Online]. Available: https://api.semanticscholar.org/CorpusID:118357515

    2007

  5. [13]

    Graph2Tac: Online repre- sentation learning of formal math concepts,

    L. Blaauwbroek, M. Ol ˇs´ak, J. Rute, F. I. Schaposnik Massolo, J. Piepenbrock, and V . Pestun, “Graph2Tac: Online repre- sentation learning of formal math concepts,” inProceedings of the 41st International Conference on Machine Learning, ser. Proceedings of Machine Learning R...

    2024

  6. [15]

    The tactician: A seamless, interactive tactic learner and prover for coq,

    L. Blaauwbroek, J. Urban, and H. Geuvers, “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: Springer-Ver...

    2020 doi

  7. [17]

    Generating correctness proofs with neural networks,

    A. Sanchez-Stern, Y . Alhessi, L. Saul, and S. Lerner, “Generating correctness proofs with neural networks,” in Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, ser. MAPL 2020. New York, NY , USA: Association for Computin...

    2020

  8. [18]

    Passport: Improving automated formal verification using identifiers,

    A. Sanchez-Stern, E. First, T. Zhou, Z. Kaufman, Y . Brun, and T. Ringer, “Passport: Improving automated formal verification using identifiers,”ACM Trans. Program. Lang. Syst., vol. 45, no. 2, Jun. 2023. [Online]. Available: https://doi.org/10.1145/3593374

    2023 doi

  9. [20]

    Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving,

    R. Xin, C. Xi, J. Yang, F. Chen, H. Wu, X. Xiao, Y . Sun, S. Zheng, and K. Shen, “Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving,” 2025. [Online]. Available: https://arxiv.org/abs/2502.03438

    2025

  10. [21]

    Deepseek- prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition,

    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, “Deepseek- prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition,”...

    2025 arXiv

  11. [22]

    Real-prover: Retrieval augmented lean prover for mathematical reasoning,

    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, “Real-prover: Retrieval augmented lean prover for mathematical reasoning,” 2025. [Online]. Available: https://arxiv.org/abs/2505.20613

    2025

  12. [24]

    Minif2f: a cross-system benchmark for formal olympiad-level mathematics,

    K. Zheng, J. M. Han, and S. Polu, “Minif2f: a cross-system benchmark for formal olympiad-level mathematics,”arXiv preprint arXiv:2109.00110, 2021

    2021 arXiv

  13. [25]

    Proofnet: Autoformalizing and formally proving undergraduate-level mathematics,

    Z. Azerbayev, B. Piotrowski, H. Schoelkopf, E. W. Ayers, D. Radev, and J. Avigad, “Proofnet: Autoformalizing and formally proving undergraduate-level mathematics,” 2023. [Online]. Available: https://arxiv.org/abs/2302.12433

    2023 arXiv

  14. [27]

    Available: http://arxiv.org/abs/1905.09381

    [Online]. Available: http://arxiv.org/abs/1905.09381

    1905 arXiv

  15. [28]

    Holist: An environment for machine learning of higher order logic theorem proving,

    K. Bansal, S. Loos, M. Rabe, C. Szegedy, and S. J. Wilcox, “Holist: An environment for machine learning of higher order logic theorem proving,” inThirty-sixth International Conference on Machine Learning (ICML), 2019. [Online]. Available: https://arxiv.org/abs/1904.03241

    2019 arXiv

  16. [29]

    Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition,

    G. Tsoukalas, J. Lee, J. Jennings, J. Xin, M. Ding, M. Jennings, A. Thakur, and S. Chaudhuri, “Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition,”

  17. [30]

    Toward a verified relational database management system,

    G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky, “Toward a verified relational database management system,” inProceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL ’10. New York, NY , USA: Association for Computing ...

  18. [31]

    Formal verification of a realistic compiler,

    X. Leroy, “Formal verification of a realistic compiler,” Commun. ACM, vol. 52, no. 7, p. 107–115, Jul. 2009. [Online]. Available: https://doi.org/10.1145/1538788.1538814

    2009

  19. [32]

    sel4: formal verification of an os kernel,

    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, “sel4: formal verification of an os kernel,” inProceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Prin...

    2009

  20. [33]

    Verdi: a framework for implementing and formally verifying distributed systems,

    J. R. Wilcox, D. Woos, P. Panchekha, Z. Tatlock, X. Wang, M. D. Ernst, and T. Anderson, “Verdi: a framework for implementing and formally verifying distributed systems,” inProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PL...

    2015

  21. [34]

    From intuition to coq: A case study in verified response-time analysis 1 of fifo scheduling,

    K. Bedarkar, M. Vardishvili, S. Bozhko, M. Maida, and B. B. Brandenburg, “From intuition to coq: A case study in verified response-time analysis 1 of fifo scheduling,” in2022 IEEE Real- Time Systems Symposium (RTSS), 2022, pp. 197–210

    2022

  22. [35]

    Torchlean: Formalizing neural networks in lean,

    R. J. George, J. Cruden, X. Zhong, H. Zhang, and A. Anandkumar, “Torchlean: Formalizing neural networks in lean,” 2026. [Online]. Available: https://arxiv.org/abs/2602. 22631

    2026

  23. [36]

    A Formal Link Between Response Time Analysis and Network Calculus (Artifact),

    P. Roux, S. Quinton, and M. Boyer, “A Formal Link Between Response Time Analysis and Network Calculus (Artifact),” Dagstuhl Artifacts Series, vol. 8, no. 1, pp. 3:1–3:3, 2022. [Online]. Available: https://drops.dagstuhl.de/entities/document/ 10.4230/DARTS.8.1.3

    2022 doi

  24. [37]

    Foundational Response-Time Analysis as Explainable Evidence of Timeliness (Artifact),

    M. Maida, S. Bozhko, and B. B. Brandenburg, “Foundational Response-Time Analysis as Explainable Evidence of Timeliness (Artifact),”Dagstuhl Artifacts Series, vol. 8, no. 1, pp. 7:1–7:2,

  25. [38]

    Thor: Wielding hammers to integrate language models and automated theorem provers,

    A. Q. Jiang, W. Li, S. Tworkowski, K. Czechowski, T. Odrzyg ´o´zd´z, P. Mił o ´s, Y . Wu, and M. Jamnik, “Thor: Wielding hammers to integrate language models and automated theorem provers,” inAdvances in Neural Information Processing Systems, vol. 35. Curran Associates, Inc., ...

    2022

  26. [39]

    Leandojo: Theorem proving with retrieval-augmented language models,

    K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. J. Prenger, and A. Anandkumar, “Leandojo: Theorem proving with retrieval-augmented language models,” inAdvances in Neural Information Processing Systems, vol. 36. Curran Associates, Inc., 2023, pp. 21 573–21 ...

    2023

  27. [40]

    Proof artifact co-training for theorem proving with language models,

    J. M. Han, J. Rute, Y . Wu, E. Ayers, and S. Polu, “Proof artifact co-training for theorem proving with language models,” inInternational Conference on Learning Representations,

  28. [41]

    Available: https://openreview.net/forum?id= rpxJc9j04U

    [Online]. Available: https://openreview.net/forum?id= rpxJc9j04U

  29. [42]

    Rango: Adaptive retrieval-augmented proving for automated software verification,

    K. Thompson, N. Saavedra, P. Carrott, K. Fisher, A. Sanchez- Stern, Y . Brun, J. a. F. Ferreira, S. Lerner, and E. First, “Rango: Adaptive retrieval-augmented proving for automated software verification,” inProceedings of the IEEE/ACM 47th International Conference on Software ...

    2025

  30. [43]

    Worst case timing requirement of real-time tasks with time redundancy,

    H. Lee, H. Shin, and S.-L. Min, “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), 1999, pp. 410– 414

    1999

  31. [44]

    LISA: Language models of ISAbelle proofs,

    A. Q. Jiang, W. Li, J. M. Han, and Y . Wu, “LISA: Language models of ISAbelle proofs,” in6th Conference on Artificial Intelligence and Theorem Proving (AITP), Aussois, France, Sep. 2021, pp. 17:1–17:3. [Online]. Available: https://aitp-conference.org/2021/abstract/paper 17.pdf

    2021

  32. [45]

    Generative language modeling for automated theorem proving,

    S. Polu and I. Sutskever, “Generative language modeling for automated theorem proving,”ArXiv, vol. abs/2009.03393, 2020. [Online]. Available: https://api.semanticscholar.org/CorpusID: 221535103

    2009 arXiv

  33. [46]

    Preemptively scheduling hard-real-time sporadic tasks on one processor,

    S. Baruah, A. Mok, and L. Rosier, “Preemptively scheduling hard-real-time sporadic tasks on one processor,” in[1990] Proceedings 11th Real-Time Systems Symposium, 1990, pp. 182–190. APPENDIX A. Illustrative Example withWORST-CASETIMINGREQUIREMENTS OFREAL-TIMETASKS WITHTIMEREDUNDANCY

    1990

  34. [48]

    Diversity-driven automated formal verification,

    E. First and Y . Brun, “Diversity-driven automated formal verification,” inProceedings of the 44th International Conference on Software Engineering, ser. ICSE ’22. New York, NY , USA: Association for Computing Machinery, 2022, p. 749–761. [Online]. Available: https://doi.org/1...

    2022

  35. [49]

    Tactok: semantics-aware proof synthesis,

    E. First, Y . Brun, and A. Guha, “Tactok: semantics-aware proof synthesis,” vol. 4, no. OOPSLA, Nov. 2020. [Online]. Available: https://doi.org/10.1145/3428299

    2020 doi

  36. [51]

    type": "definition

    Extracted JSON and Informal Sketch for Illustrative Example:Listing 3 presents the extracted json that is used for the Section VI. Listing 3: Structured extraction of Definition 1 and Claim 1 [ { "type": "definition", "identifier": "Definition 1", "formal_description": { "stat...

  37. [52]

    Faults are transient or intermittent

  38. [53]

    Intuition for generating code: The total time a task needs is its normal execution time plus the maximum possible time spent on fault detection, recovery, and re-execution

    Faults are detected immediately upon occurrence Conclusion: Defines the total time a task requires to complete its execution and recovery actions. Intuition for generating code: The total time a task needs is its normal execution time plus the maximum possible time spent on fa...

  39. [54]

    Identify the base execution time without faults W_i_0

  40. [55]

    Calculate the maximum overhead A_i_k_i based on the specific redundancy technique used

  41. [56]

    Sum them to find the total timing requirement Key Insights:

  42. [57]

    Separates the functional execution time from the fault-tolerance overhead *) (* ====section==== claim Claim 1 Statement: W_i_k_i = k_i * (R_star + W_i_0) + W_i_0 Variables: W_i_k_i: Worst case timing requirement for retry k_i: Number of faults R_star: Task restart overhead (co...

  43. [58]

    Intuition for generating code: If a fault occurs, the task loses all progress and must restart

    Task must restart from the very beginning after every fault Conclusion: Calculates the WCTR for the Retry redundancy technique. Intuition for generating code: If a fault occurs, the task loses all progress and must restart. In the worst case, a fault occurs just before complet...

  44. [59]

    For each of the k_i faults, add the cost of a full restart (R_star) and a full re-execution (W_i_0)

  45. [60]

    Add the final successful execution time (W_i_0) Key Insights:

  46. [61]

    schedulability analysis

    Retry is the most expensive technique because it discards all work done prior to the fault *) B. IEEE Xplore API query We queried IEEE Xplore using schedulability-analysis and real-time-systems keywords. ("schedulability analysis" OR "schedulability" OR "response time analysis...

  47. [62]

    Preemptively Scheduling Hard-Real-Time Sporadic Tasks on One Processor

    Source Material and Extraction:We consider the paper“Preemptively Scheduling Hard-Real-Time Sporadic Tasks on One Processor”[46] as a representative example. From this paper, we extract the following definitions and lemma. In particular, the lemmaOptimality of the Deadline Alg...

  48. [64]

    e_i, d_i, p_i are positive integers

  49. [66]

    Represent each task task_i by execution time e_i, deadline d_i, and minimum separation p_i

  50. [67]

    Require e_i <= d_i so that each individual job can fit inside its own deadline window

  51. [68]

    Require e_i <= p_i so that the task does not request more execution than its minimum inter-arrival spacing can plausibly support

  52. [69]

    Key Insights:

    Collect all tasks into task_system. Key Insights:

  53. [70]

    The minimum separation p_i is the key distinction between sporadic and arbitrary aperiodic arrivals

  54. [71]

    *) (* ====section==== definition Definition 2 Statement: Let P = lcm(p_1, p_2, ..., p_n)

    The model allows d_i > p_i, so jobs of the same task may have overlapping deadline windows. *) (* ====section==== definition Definition 2 Statement: Let P = lcm(p_1, p_2, ..., p_n). A request of task_i at time t_0 is represented by request_i_t_0 = i, t_0. The request requires ...

  55. [72]

    task_i belongs to task_system

  56. [73]

    Intuition for generating code: A sporadic task generates individual requests or jobs

    time is discrete Conclusion: Defines task requests and their execution windows. Intuition for generating code: A sporadic task generates individual requests or jobs. A request released at t_0 must receive e_i units of service before its absolute deadline t_0 + d_i. Steps for g...

  57. [74]

    Take a task task_i and release time t_0

  58. [75]

    Construct request_i_t_0

  59. [76]

    Set the absolute deadline to t_0 + d_i

  60. [77]

    Key Insights:

    Require the scheduler to allocate e_i time units inside [t_0, t_0 + d_i). Key Insights:

  61. [78]

    Schedulability is checked over requests, not just over task parameters

  62. [79]

    The absolute deadline is release_time plus relative deadline. *) (* ====section==== definition Definition 3 Statement: A set of requests request_set is schedulable iff there exists a processor schedule that allocates e_i time units to every request request_i_t_0 in request_set...

  63. [81]

    Intuition for generating code: A request set is legal if it respects the sporadic separation constraints

    all requests satisfy their task parameters Conclusion: Defines schedulability of a request set, legality of arrivals, and feasibility of a sporadic task system. Intuition for generating code: A request set is legal if it respects the sporadic separation constraints. A task sys...

  64. [82]

    Check all pairs of requests of the same task

  65. [83]

    If any two releases are closer than p_i, the request set is illegal

  66. [84]

    If the request set is legal, ask whether a valid preemptive single-processor schedule exists

  67. [85]

    Key Insights:

    The task system is feasible only when every legal request set has such a schedule. Key Insights:

  68. [86]

    Feasibility is a universal property over all legal arrival sequences

  69. [87]

    The difficulty comes from the unbounded number of possible legal sporadic request sets. *) (* ====section==== definition Definition 4 Statement: An online scheduling algorithm U maps each request_set and time t to either a selected active request request_i_t_0, an idle decisio...

  70. [88]

    requests are presented to U at their release times

  71. [89]

    U is online and iterative

  72. [90]

    Intuition for generating code: At each time, the scheduler either runs one active request or idles

    preemption is allowed at integer time boundaries Conclusion: Defines online scheduling, active requests, and failure. Intuition for generating code: At each time, the scheduler either runs one active request or idles. Failure occurs exactly when a request reaches its deadline ...

  73. [91]

    At each time t, identify all active requests

  74. [92]

    Choose one active request to execute or leave the processor idle

  75. [93]

    Update the amount of service received by the chosen request

  76. [94]

    Key Insights:

    If any request reaches its deadline without receiving e_i service, report failure. Key Insights:

  77. [95]

    Failure is defined at the deadline boundary

  78. [96]

    *) (* ====section==== definition Definition 5 Statement: The deadline algorithm U allocates the processor at time t to the active request with the nearest absolute deadline

    The active-request definition captures unfinished jobs that are still eligible to execute. *) (* ====section==== definition Definition 5 Statement: The deadline algorithm U allocates the processor at time t to the active request with the nearest absolute deadline. For active r...

  79. [98]

    Intuition for generating code: The deadline algorithm is earliest-deadline-first with a deterministic tie-breaking rule

    ties are broken by lower task index Conclusion: Defines the deadline-driven scheduling algorithm used throughout the paper. Intuition for generating code: The deadline algorithm is earliest-deadline-first with a deterministic tie-breaking rule. The request whose deadline is cl...

  80. [99]

    At time t, collect all active requests

  81. [100]

    Compute each active request’s absolute deadline

  82. [101]

    Select the request with the smallest absolute deadline

  83. [102]

    Key Insights:

    If two requests have the same absolute deadline, choose the one with smaller task index. Key Insights:

  84. [103]

    The algorithm is EDF specialized to the paper’s request model

  85. [104]

    *) (* ====section==== lemma Lemma 1 Statement: The deadline_algorithm_U is optimal for sporadic task systems

    Tie-breaking does not affect whether failure occurs, but makes the schedule deterministic. *) (* ====section==== lemma Lemma 1 Statement: The deadline_algorithm_U is optimal for sporadic task systems. Given any request_set, U constructs a schedule for request_set if one exists...

  86. [105]

    preemptive scheduling

  87. [106]

    sporadic request model

  88. [107]

    legal request sets respect minimum separations Conclusion: EDF-style deadline scheduling is sufficient to decide feasibility over legal request sets. Intuition for generating code: For preemptive uniprocessor scheduling, always running the active job with the earliest deadline...

  89. [108]

    Consider any legal request set

  90. [109]

    Run the deadline algorithm on that request set

  91. [110]

    If any feasible schedule exists, the deadline algorithm also succeeds

  92. [111]

    If the deadline algorithm fails, no feasible schedule exists for that request set

  93. [112]

    Key Insights:

    Thus task_system is feasible exactly when the deadline algorithm never fails on any legal request set. Key Insights:

  94. [113]

    This lemma lets the paper focus on one canonical scheduler rather than all possible schedules

  95. [114]

    *) The extraction is alsodependency-aware

    It converts feasibility into absence of failure under the deadline algorithm. *) The extraction is alsodependency-aware. For each invariant, we record its dependencies on previously introduced invariants, inducing a partial order for formalization. An invariant is formalized o...

  96. [115]

    To support this translation, we employ retrieval-augmented generation (RAG) over the PROSAcodebase

    Retrieval-Augmented Generation:Given the informal sketch of an invariant, the next step is to translate it into a PROSA script. To support this translation, we employ retrieval-augmented generation (RAG) over the PROSAcodebase. We use the statement,conclusion, andintuitionfiel...

  97. [116]

    Listing 6: Skeleton code generated from the informal sketch

    Skeleton Code Generation:Using the retrieved context, we prompt the LLM to generateskeleton code—a structurally complete, type-checkable PROSAscript in which all imports, section boundaries, type-class contexts, variable declarations, and definition bodies are fully specified,...

  98. [117]

    Providing the full skeleton gives the model access to surrounding definitions, instances, and auxiliary lemmas, improving proof generation

    Proof 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, ...

  99. [2019]

    Available: http://arxiv.org/abs/1910.09336

    [Online]. Available: http://arxiv.org/abs/1910.09336

    1910 arXiv

  100. [2022]

    Available: https://drops.dagstuhl.de/entities/ document/10.4230/DARTS.8.1.7

    [Online]. Available: https://drops.dagstuhl.de/entities/ document/10.4230/DARTS.8.1.7

    doi

  101. [2024]

    Available: https://arxiv.org/abs/2407.11214

    [Online]. Available: https://arxiv.org/abs/2407.11214

    arXiv

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.