ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems

Eric Vin; Lucy Horowitz; Kyle A. Miller; Inigo Incer; Sanjit A. Seshia; Daniel J. Fremont

cs.LONov 4, 2025

ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems

Authors: Eric Vin, Lucy Horowitz, Kyle A. Miller, Inigo Incer, Sanjit A. Seshia, Daniel J. Fremont

Organizations: University of California, Santa Cruz, Santa Cruz CA 95064, USA · University of Michigan, Ann Arbor MI 48109, USA · University of California, Berkeley, Berkeley CA 94720, USA

Abstract

Full verification of learning-enabled cyber-physical systems (CPS) has long been intractable due to challenges including black-box components and complex real-world environments. Existing tools either provide formal guarantees for limited types of systems or test the system as a monolith, but no general framework exists for compositional analysis of learning-enabled CPS using varied verification techniques over complex real-world environments. This paper introduces a tool, ScenicProver, that aims to fill this gap by enabling the construction of sound, formally-checked assurance cases for CPS. ScenicProver is backed by a formal theory, which we lay out in this paper. ScenicProver supports: (1) environment modeling using the Scenic probabilistic programming language; (2) compositional system modeling with clear component interfaces, ranging from interpretable code to black boxes; (3) assume-guarantee contracts over those components using an extension of Linear Temporal Logic containing arbitrary Scenic expressions; (4) evidence generation through testing, formal proofs in Lean 4, and external assumptions; (5) sound combination of generated evidence using contract operators with Pacti; and (6) automatic generation of assurance cases tracking the provenance of system-level guarantees. We demonstrate its effectiveness through two case studies: one on an automatic emergency braking system with sensor fusion and one on drone safety. By leveraging manufacturer guarantees for sensors and focusing testing effort on uncertain conditions, our approach enables stronger probabilistic guarantees than monolithic testing with the same computational budget.

Figures & tables

Figure 1: The structure of the system in our motivating example.

Figure 2: A ScenicProver snippet defining the throttle controller component of the AEB example from Sec. 2 .

Figure 3: An abbreviated ScenicProver snippet defining a contract over a component which overrides the throttle controller to apply emergency braking if the lead car is too close.

Figure 4: The structure of the AEB assurance case.

Panel of Figure 5 — Figure 5: Probability lower bounds for the top-level case study contracts, as a function of time spent testing.

Appendix figures & tables4 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 6: Probability lower bounds on the overall system contract ( Keeps Distance ) obtained with ScenicProver, as a function of number of simulations run.

Figure 7: Probability lower bounds on the overall system contract ( CorridorContainment ) obtained with ScenicProver, as a function of number of simulations run.

Figure 8: The structure of the drone assurance case.

Parameter	Value
Minimum clearance from wall and floor (safety)	$1\,\mathrm{m}$
Controller target clearance	$3.2\,\mathrm{m}$
Maximum commanded approach rate (wall / floor)	$2$ / $1.5\,\mathrm{m/s}$
Maximum GNSS error under poor reception	$1.5\,\mathrm{m}$
VIO rated horizontal wind	$\leq 6\,\mathrm{m/s}$
Sensor error bound under rated conditions	$0.3\,\mathrm{m}$

Appendix

Table 1: Parameters for the drone case study.

Formal Verification

Formal verification uses mathematical models and machine-checked proofs to establish whether software and systems satisfy precise specifications.

See all 354 papers

Assuring Learning-Enabled Cyber-Physical Systems with Foundation Models: A Neuro-Symbolic Agenda for Testing, Verification, and Runtime Assurance
Oct 29, 2026Xi Zheng, Ivan Ruchkin, Hong Jin Kang +11Cyber-Physical Systems Runtime Assurance
Macquarie University, Australia · University of Florida, USA · University of Sydney, Australia +11
Large Language Models as Falsifiers for Cyber-Physical Systems
Sep 17, 2026Ali ArjomandBigdeli, Jiawei Zhou, Stanley BakCyber-Physical Systems Large Language Model-Guided Optimization
Stony Brook University, Stony Brook, New York, USA
SMC-ES: Automated synthesis of formally verified control policies
Jul 16, 2026Riccardo Curcio, Toni Mancini, Enrico TronciStatistical Model Checking Formal Verification
Department of Computer Science, Sapienza University of Rome, via Salaria 113, 00198 Rome, Italy

Oct 29, 2026J/K move · Enter open · S save

Assuring Learning-Enabled Cyber-Physical Systems with Foundation Models: A Neuro-Symbolic Agenda for Testing, Verification, and Runtime Assurance

Xi Zheng, Ivan Ruchkin, Hong Jin Kang, Tevfik Bultan+10

Macquarie University, Australia · University of Florida, USA · University of Sydney, Australia+11

Cyber-Physical Systems Runtime Assurance Formal Verification Neuro-Symbolic Reasoning

Open paper AskPDF arXiv

Learning-enabled cyber-physical systems (CPS), including autonomous vehicles and UAVs, increasingly incorporate foundation models, yet fragmented assurance practices provide insufficient support for system-level guarantees. We argue that restoring engineering control across stochastic neural, symbolic, and physical boundaries requires a shift from model-centric evaluation to system-level assurance. We introduce the Foundation Model Assurance Stack, connecting three directions: (i) neuro-symbolic architectures that constrain foundation models through explicit symbolic world models, reasoning layers, and interfaces; (ii) semantically grounded, conformance-based testing that combines formal specifications and symbolic world models with foundation-model-assisted specification mining, scenario generation, and test synthesis; and (iii) compositional verification and runtime assurance that target formally tractable components and interfaces through modular contracts, equivalence checking, verified synthesis, uncertainty-aware reasoning, and runtime monitoring and enforcement. Symbolic abstractions establish assurance boundaries between stochastic learning and formal reasoning, connecting testing, verification, and runtime evidence across the system lifecycle. Foundation models serve as constrained assistants whose outputs are independently checked wherever correctness can be formally specified. We identify research challenges in specification engineering, abstraction fidelity, evidence composition, and lifecycle certification, and outline a staged agenda toward trustworthy, deployable, and certifiable learning-enabled CPS.

Abstract

Formal Verification

Explore similar work

Assuring Learning-Enabled Cyber-Physical Systems with Foundation Models: A Neuro-Symbolic Agenda for Testing, Verification, and Runtime Assurance

Large Language Models as Falsifiers for Cyber-Physical Systems

SMC-ES: Automated synthesis of formally verified control policies