ProsaBuddy: Assisting Mechanized Real-Time Schedulability Analysis with LLM-based Agents

Excerpt

arXiv:2610.03796v1 Announce Type: cross Abstract: Rigorous schedulability analysis is essential for the design of hard real-time systems, yet errors in pen-and-paper proofs threaten the safety of critical applications. The Prosa initiative addresses this by offering a foundation for building machine-checkable schedulability analysis proofs in the Rocq proof assistant. However, the substantial time and expertise required to construct such proofs remain a major barrier for wider adoption of Prosa.