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

arXiv: https://arxiv.org/abs/2511.02164 · HTML: https://mlsanity.com/paper/2511.02164/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 44 references that are in the map.
- First posted on arXiv 4 Nov 2025.

## Builds on (most cited first, 15 of 15)

- [Scenic: A Language for Scenario Specification and Scene Generation](https://mlsanity.com/paper/1809.09310/) (2018)
- [Adaptive Stress Testing for Autonomous Vehicles](https://mlsanity.com/paper/1902.01909/) (2019)
- [A Survey of Algorithms for Black-Box Safety Validation of Cyber-Physical Systems](https://mlsanity.com/paper/2005.02979/) (2020)
- [Shield Synthesis: Runtime Enforcement for Reactive Systems](https://mlsanity.com/paper/1501.02573/) (2015)
- [Scenic: A Language for Scenario Specification and Data Generation](https://mlsanity.com/paper/2010.06580/) (2020)
- [Compositional Falsification of Cyber-Physical Systems with Machine Learning Components](https://mlsanity.com/paper/1703.00978/) (2017)
- [SOTER: A Runtime Assurance Framework for Programming Safe Robotics Systems](https://mlsanity.com/paper/1808.07921/) (2018)
- [Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study](https://mlsanity.com/paper/2302.04634/) (2023)
- [Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)](https://mlsanity.com/paper/2204.13693/) (2022)
- [Compositional Verification for Autonomous Systems with Deep Learning Components](https://mlsanity.com/paper/1810.08303/) (2018)
- [3D Environment Modeling for Falsification and Beyond with Scenic 3.0](https://mlsanity.com/paper/2307.03325/) (2023)
- [Decidable Fragments of LTLf Modulo Theories (Extended Version)](https://mlsanity.com/paper/2307.16840/) (2023)
- [Verse: A Python library for reasoning about multi-agent hybrid system scenarios](https://mlsanity.com/paper/2301.08714/) (2023)
- [Some Algebraic Aspects of Assume-Guarantee Reasoning](https://mlsanity.com/paper/2309.08875/) (2023)
- [LeanLTL: A unifying framework for linear temporal logics in Lean](https://mlsanity.com/paper/2507.01780/) (2025)

## Built on by (most cited first, 2 of 2)

- [Position: A Three-Layer Probabilistic Assume-Guarantee Architecture Is Structurally Required for Safe LLM Agent Deployment](https://mlsanity.com/paper/2605.18672/) (2026)
- [Scenario-Based Compositional Statistical Model Checking for Safety Specifications](https://mlsanity.com/paper/2610.05571/) (2026)

## Abstract (arXiv)

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 ScenicProver, a verification framework that aims to fill this gap. Built upon the Scenic probabilistic programming language, the framework supports: (1) compositional system description with clear component interfaces, ranging from interpretable code to black boxes; (2) assume-guarantee contracts over those components using an extension of Linear Temporal Logic containing arbitrary Scenic expressions; (3) evidence generation through testing, formal proofs via Lean 4 integration, and importing external assumptions; (4) systematic combination of generated evidence using contract operators; and (5) automatic generation of assurance cases tracking the provenance of system-level guarantees. We demonstrate the framework's effectiveness through a case study on an autonomous vehicle's automatic emergency braking system with sensor fusion. By leveraging manufacturer guarantees for radar and laser sensors and focusing testing efforts on uncertain conditions, our approach enables stronger probabilistic guarantees than monolithic testing with the same computational budget.