ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
Eric Vin, Kyle A. Miller, Inigo Incer, Sanjit A. Seshia, Daniel J. Fremont
cs.LO
Nov 4, 2025 · v1
TL;DR
Generates formal proofs of component contracts via Lean 4 integration within a compositional probabilistic verification framework.
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 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.
Problem
Full verification of learning-enabled cyber-physical systems is intractable due to black-box components and complex environments. No general framework exists for compositional analysis using varied verification techniques over complex real-world environments.
Approach
ScenicProver is built on the Scenic probabilistic programming language and supports compositional system description with clear component interfaces, assume-guarantee contracts using an extension of Linear Temporal Logic, evidence generation through testing and formal proofs via Lean 4 integration, systematic combination of evidence using contract operators, and automatic generation of assurance cases. The framework enables mixing formal proofs with statistical testing results.
Results
A case study on an autonomous vehicle's automatic emergency braking system with sensor fusion demonstrates that the framework enables stronger probabilistic guarantees than monolithic testing alone, by leveraging manufacturer guarantees for radar and laser sensors and focusing testing efforts on uncertain conditions.
