Verse Library
A Python library for creating, simulating and formally verifying scenarios with multiple interacting, decision-making agents, such as autonomous vehicles, using hybrid reachability analysis.
Verse lets a developer define scenario agents whose decision logic is written in an expressive subset of Python, while each agent's continuous motion is described as a black-box function; a scenario combines several such agents with a map and a sensor that defines how the agents perceive each other. Agents can be ported across different maps, which can be built from scratch or imported from OpenDRIVE files.
Scenarios can be simulated directly or verified with hybrid reachability analysis: the initial implementation represents reachable sets as intervals, or hyperrectangles, and a newer implementation supporting a different reachable-set representation is in progress. An optional NeuReach backend, added through a git submodule, provides an alternative continuous-post operator alongside the built-in DryVR backend. It requires Python 3.8 or later, installs with pip, and includes an interactive Jupyter tutorial and worked demos such as a bouncing-ball scenario. It is developed by the Reliable Autonomy Research Group at the University of Illinois at Urbana-Champaign.