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

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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.
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.
ParameterValue
Minimum clearance from wall and floor (safety)1 m1\,\mathrm{m}
Controller target clearance3.2 m3.2\,\mathrm{m}
Maximum commanded approach rate (wall / floor)22 / 1.5 m/s1.5\,\mathrm{m/s}
Maximum GNSS error under poor reception1.5 m1.5\,\mathrm{m}
VIO rated horizontal wind≤6 m/s\leq 6\,\mathrm{m/s}
Sensor error bound under rated conditions0.3 m0.3\,\mathrm{m}
Appendix
Table 1: Parameters for the drone case study.
More in this topic

Formal Verification

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

See all 354 papers

Explore similar work

CardsList
Oct 29, 2026

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

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.

Xi Zheng, Ivan Ruchkin, Hong Jin Kang +11

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

Cyber-Physical SystemsRuntime AssuranceFormal VerificationNeuro-Symbolic Reasoning
AskPDF
Sep 17, 2026

Large Language Models as Falsifiers for Cyber-Physical Systems

Falsification searches for counterexamples to formal specifications in cyber-physical systems (CPS). With specifications written in Signal Temporal Logic (STL), falsification can be formulated as a robustness optimization problem, traditionally tackled with black-box search algorithms. In parallel, large language models (LLMs) have recently emerged as surprisingly effective optimizers when coupled with iterative prompting. In this work, we connect these ideas and introduce LLM-Falsifier, an LLM-based approach that falsifies specifications by minimizing the STL robustness degree. Beyond generic prompt-based optimization, our key idea is to expose the LLM to semantic information that is natural for language models but absent from standard numerical optimizers, including natural-language input and output names, output trajectories, and critical-time witnesses for the minimum robustness value. These additions enable smarter and more sample-efficient robustness search. On the ARCH-COMP falsification benchmarks, LLM-Falsifier is shown to outperform existing falsification tools based on a range of optimization paradigms, from surrogate-based and Bayesian optimization to search-based testing, on 14 of 21 specifications when measured by the average number of simulations required to find a counterexample.

Ali ArjomandBigdeli, Jiawei Zhou, Stanley Bak

Stony Brook University, Stony Brook, New York, USA

Cyber-Physical SystemsLarge Language Model-Guided Optimization
AskPDF
Jul 16, 2026

SMC-ES: Automated synthesis of formally verified control policies

The deployment of autonomous cyber-physical systems in safety-critical environments requires closed-loop control strategies (i.e., policies) that are not only performant but also provably safe and robust. While learning-based methodologies such as Reinforcement Learning offer flexible and scalable approaches to automatically synthesize such controllers, they typically lack the formal guarantees necessary for safe deployment. To bridge this gap, we propose a novel simulation-based methodology to automatically synthesize policies with formal guarantees regarding performance, safety, and robustness specifications. Specifically, given a set of properties to verify, a confidence parameter δδ and an allowable failure probability ε\varepsilon, our method guarantees that the synthesized policy comes with a certificate: with confidence at least 1−δ1 - δ, the probability of encountering a scenario where the given properties are violated is at most ε\varepsilon. We demonstrate the feasibility of our approach by developing SMC-ES, an algorithm that integrates Evolutionary Strategies with Statistical Model Checking-based verification. We evaluate SMC-ES on a suite of continuous control tasks using Gymnasium and Safety Gymnasium testbeds. Results show that, at the price of a sustainable increase in computational cost, our algorithm provides formal guarantees regarding performance, safety, and robustness specifications, while performing competitively against leading model-free Deep Reinforcement Learning (DRL) and Safe-DRL baselines.

Riccardo Curcio, Toni Mancini, Enrico Tronci

Department of Computer Science, Sapienza University of Rome, via Salaria 113, 00198 Rome, Italy

Statistical Model CheckingFormal VerificationSafe RLRobust RL
AskPDF