Safety-critical cyber-physical systems increasingly use reinforcement learning-based controllers, yet existing engineering methodologies cannot assure these systems’ safety. Assuring safety requires connecting three concerns that are currently addressed in isolation: the system’s design, the reinforcement learning pipeline, and runtime verification. This paper introduces CLARITY, a system that ingests designs written in SysML v2 and, through novel translational semantics to the nuXmv model checker, verifies safety requirements, synthesizes a reinforcement learning pipeline, and generates a runtime monitor. CLARITY enables fully traceable safety assurance arguments for reinforcement learning-based systems, closing the gap between system design, controller synthesis, and runtime assurance. We validate CLARITY on three CPS benchmarks of increasing complexity, demonstrating verified safety requirements, effective learned controllers, and lightweight runtime monitoring from a single SysML v2 specification.

@inproceedings{paperbot12609,
  title = {Clarity: From Formal System Designs to Verified RL Controllers},
  author = {Austin O'Quinn and Conor Snedeker and Max Taylor and Lance Joneckis and Christopher Stewart},
  booktitle = {ASE},
  year = {2026},
  doi = {10.1145/3832783.3834429}
}