VeriGym¶

From Deep Reinforcement Learning Simulators to Verifiable Models and Back¶

verigym is a modular and comprehensive open-source framework to bridge Reinforcement Learning (RL) and Probabilistic Model Checking (PMC) research. verigym exposes an abstraction interface to convert simulator-based RL environments following the Gymnasium API into explicit model formats supported by state-of-the-art PMC and synthesis tools such as Storm and PRISM. verigym maps solutions back to the original environment, e.g., for direct deployment or to guide RL training.

A high-level overview over the VeriGym pipeline

uv pip install verigym
# alternatively using pip
pip install verigym

Getting Started¶

If you want to use verigym check out the installation guide.
If you want to contribute, check out the contribution guide. Pick up an issue or leave us one!

Examples¶

We provide guides with walk-throughs through central VeriGym functionality, and workflows with end-to-end implementations of several tasks, including:

learning a model checkable MDP from a continuous environment
abstraction refinement
shielding
adding external frameworks

API Reference¶

Includes full code documentation.